sbth - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem sbth 4437

Description: Schroeder-Bernstein Theorem. Theorem 18 of [Suppes] p. 95. This theorem states that if set A is smaller (has lower cardinality) than B and vice-versa, then A and B are equinumerous (have the same cardinality). The interesting thing is that this can be proved without invoking the Axiom of Choice, as we do here, but the proof as you can see is quite difficult. (The theorem can be proved more easily if we allow AC.) The main proof consists of lemmas sbthlem1 4427 through sbthlem10 4436; this final piece mainly changes bound variables to eliminate the hypotheses of sbthlem10 4436. We follow closely the proof in Suppes, which you should consult to understand our proof at a higher level.

**Assertion**
Ref	Expression
sbth	⊢ ((A ≼ B ⋀ B ≼ A) → A ≈ B)

**Proof of Theorem sbth**
Step	Hyp	Ref	Expression
1		breq1 2612	. . . . . 6 ⊢ (z = A → (z ≼ w ↔ A ≼ w))
2		breq2 2613	. . . . . 6 ⊢ (z = A → (w ≼ z ↔ w ≼ A))
3	1, 2	anbi12d 626	. . . . 5 ⊢ (z = A → ((z ≼ w ⋀ w ≼ z) ↔ (A ≼ w ⋀ w ≼ A)))
4		breq1 2612	. . . . 5 ⊢ (z = A → (z ≈ w ↔ A ≈ w))
5	3, 4	imbi12d 624	. . . 4 ⊢ (z = A → (((z ≼ w ⋀ w ≼ z) → z ≈ w) ↔ ((A ≼ w ⋀ w ≼ A) → A ≈ w)))
6		breq2 2613	. . . . . 6 ⊢ (w = B → (A ≼ w ↔ A ≼ B))
7		breq1 2612	. . . . . 6 ⊢ (w = B → (w ≼ A ↔ B ≼ A))
8	6, 7	anbi12d 626	. . . . 5 ⊢ (w = B → ((A ≼ w ⋀ w ≼ A) ↔ (A ≼ B ⋀ B ≼ A)))
9		breq2 2613	. . . . 5 ⊢ (w = B → (A ≈ w ↔ A ≈ B))
10	8, 9	imbi12d 624	. . . 4 ⊢ (w = B → (((A ≼ w ⋀ w ≼ A) → A ≈ w) ↔ ((A ≼ B ⋀ B ≼ A) → A ≈ B)))
11		visset 1804	. . . . 5 ⊢ z ∈ V
12		sseq1 2072	. . . . . . 7 ⊢ (y = x → (y ⊆ z ↔ x ⊆ z))
13		imaeq2 3386	. . . . . . . . . 10 ⊢ (y = x → (f “ y) = (f “ x))
14	13	difeq2d 2149	. . . . . . . . 9 ⊢ (y = x → (w ∖ (f “ y)) = (w ∖ (f “ x)))
15		imaeq2 3386	. . . . . . . . 9 ⊢ ((w ∖ (f “ y)) = (w ∖ (f “ x)) → (g “ (w ∖ (f “ y))) = (g “ (w ∖ (f “ x))))
16		sseq1 2072	. . . . . . . . 9 ⊢ ((g “ (w ∖ (f “ y))) = (g “ (w ∖ (f “ x))) → ((g “ (w ∖ (f “ y))) ⊆ (z ∖ y) ↔ (g “ (w ∖ (f “ x))) ⊆ (z ∖ y)))
17	14, 15, 16	3syl 20	. . . . . . . 8 ⊢ (y = x → ((g “ (w ∖ (f “ y))) ⊆ (z ∖ y) ↔ (g “ (w ∖ (f “ x))) ⊆ (z ∖ y)))
18		difeq2 2144	. . . . . . . . 9 ⊢ (y = x → (z ∖ y) = (z ∖ x))
19	18	sseq2d 2079	. . . . . . . 8 ⊢ (y = x → ((g “ (w ∖ (f “ x))) ⊆ (z ∖ y) ↔ (g “ (w ∖ (f “ x))) ⊆ (z ∖ x)))
20	17, 19	bitrd 526	. . . . . . 7 ⊢ (y = x → ((g “ (w ∖ (f “ y))) ⊆ (z ∖ y) ↔ (g “ (w ∖ (f “ x))) ⊆ (z ∖ x)))
21	12, 20	anbi12d 626	. . . . . 6 ⊢ (y = x → ((y ⊆ z ⋀ (g “ (w ∖ (f “ y))) ⊆ (z ∖ y)) ↔ (x ⊆ z ⋀ (g “ (w ∖ (f “ x))) ⊆ (z ∖ x))))
22	21	cbvabv 1900	. . . . 5 ⊢ {y∣(y ⊆ z ⋀ (g “ (w ∖ (f “ y))) ⊆ (z ∖ y))} = {x∣(x ⊆ z ⋀ (g “ (w ∖ (f “ x))) ⊆ (z ∖ x))}
23		eqid 1468	. . . . 5 ⊢ ((f ↾ ∪{y∣(y ⊆ z ⋀ (g “ (w ∖ (f “ y))) ⊆ (z ∖ y))}) ∪ (^◡g ↾ (z ∖ ∪{y∣(y ⊆ z ⋀ (g “ (w ∖ (f “ y))) ⊆ (z ∖ y))}))) = ((f ↾ ∪{y∣(y ⊆ z ⋀ (g “ (w ∖ (f “ y))) ⊆ (z ∖ y))}) ∪ (^◡g ↾ (z ∖ ∪{y∣(y ⊆ z ⋀ (g “ (w ∖ (f “ y))) ⊆ (z ∖ y))})))
24		visset 1804	. . . . 5 ⊢ w ∈ V
25	11, 22, 23, 24	sbthlem10 4436	. . . 4 ⊢ ((z ≼ w ⋀ w ≼ z) → z ≈ w)
26	5, 10, 25	vtocl2g 1841	. . 3 ⊢ ((A ∈ V ⋀ B ∈ V) → ((A ≼ B ⋀ B ≼ A) → A ≈ B))
27		reldom 4355	. . . 4 ⊢ Rel ≼
28	27	brrelexi 3198	. . 3 ⊢ (A ≼ B → A ∈ V)
29	27	brrelexi 3198	. . 3 ⊢ (B ≼ A → B ∈ V)
30	26, 28, 29	syl2an 454	. 2 ⊢ ((A ≼ B ⋀ B ≼ A) → ((A ≼ B ⋀ B ≼ A) → A ≈ B))
31	30	pm2.43i 64	1 ⊢ ((A ≼ B ⋀ B ≼ A) → A ≈ B)

Colors of variables: wff set class

Syntax hints: → wi 3 ↔ wb 146 ⋀ wa 223 = wceq 953 ∈ wcel 955 {cab 1456 Vcvv 1802 ∖ cdif 2034 ∪ cun 2035 ⊆ wss 2037 ∪cuni 2493 class class class wbr 2609 ^◡ccnv 3159 ↾ cres 3162 “ cima 3163 ≈ cen 4348 ≼ cdom 4349

This theorem is referenced by: sbthbg 4438 sdomnsym 4442 sdomdomtr 4449 limenpsi 4485 php 4493 onomeneq 4498 unbnn 4521 xpnnen 7441 znnen 7445 qnnen 7446 infxpidmlem1 7495 infxpidmlem12 7506 infunabs 7508 infcdaabs 7509 infdif 7511 infxpabs 7513 infmap1 7516 infmap2 7523

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 959 ax-gen 960 ax-8 961 ax-9 962 ax-10 963 ax-11 964 ax-12 965 ax-13 966 ax-14 967 ax-17 968 ax-4 970 ax-5o 972 ax-6o 975 ax-9o 1119 ax-10o 1136 ax-16 1206 ax-11o 1213 ax-ext 1452 ax-rep 2683 ax-sep 2693 ax-pow 2732 ax-pr 2769 ax-un 2857

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3an 775 df-ex 978 df-sb 1168 df-eu 1375 df-mo 1376 df-clab 1457 df-cleq 1462 df-clel 1465 df-ne 1579 df-ral 1641 df-rex 1642 df-v 1803 df-dif 2039 df-un 2040 df-in 2041 df-ss 2043 df-nul 2271 df-pw 2392 df-sn 2402 df-pr 2403 df-op 2406 df-uni 2494 df-br 2610 df-opab 2657 df-id 2824 df-xp 3174 df-rel 3175 df-cnv 3176 df-co 3177 df-dm 3178 df-rn 3179 df-res 3180 df-ima 3181 df-fun 3182 df-fn 3183 df-f 3184 df-f1 3185 df-fo 3186 df-f1o 3187 df-en 4351 df-dom 4352