Theorem sbth 5331

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 5321 through sbthlem10 5330; this final piece mainly changes bound variables to eliminate the hypotheses of sbthlem10 5330. We follow closely the proof in Suppes, which you should consult to understand our proof at a higher level. Note that Suppes' proof, which is credited to J. M. Whitaker, does not require the Axiom of Infinity.

Assertion

Ref	Expression
sbth	|- ((A ~<_ B /\ B ~<_ A) -> A ~~ B)

Proof of Theorem sbth

Step	Hyp	Ref	Expression
1		breq1 3161	. . . . . 6 |- (z = A -> (z ~<_ w <-> A ~<_ w))
2		breq2 3162	. . . . . 6 |- (z = A -> (w ~<_ z <-> w ~<_ A))
3	1, 2	anbi12d 687	. . . . 5 |- (z = A -> ((z ~<_ w /\ w ~<_ z) <-> (A ~<_ w /\ w ~<_ A)))
4		breq1 3161	. . . . 5 |- (z = A -> (z ~~ w <-> A ~~ w))
5	3, 4	imbi12d 685	. . . 4 |- (z = A -> (((z ~<_ w /\ w ~<_ z) -> z ~~ w) <-> ((A ~<_ w /\ w ~<_ A) -> A ~~ w)))
6		breq2 3162	. . . . . 6 |- (w = B -> (A ~<_ w <-> A ~<_ B))
7		breq1 3161	. . . . . 6 |- (w = B -> (w ~<_ A <-> B ~<_ A))
8	6, 7	anbi12d 687	. . . . 5 |- (w = B -> ((A ~<_ w /\ w ~<_ A) <-> (A ~<_ B /\ B ~<_ A)))
9		breq2 3162	. . . . 5 |- (w = B -> (A ~~ w <-> A ~~ B))
10	8, 9	imbi12d 685	. . . 4 |- (w = B -> (((A ~<_ w /\ w ~<_ A) -> A ~~ w) <-> ((A ~<_ B /\ B ~<_ A) -> A ~~ B)))
11		visset 2128	. . . . 5 |- z e. _V
12		sseq1 2470	. . . . . . 7 |- (y = x -> (y C_ z <-> x C_ z))
13		imaeq2 4071	. . . . . . . . . 10 |- (y = x -> (f"y) = (f"x))
14	13	difeq2d 2558	. . . . . . . . 9 |- (y = x -> (w \ (f"y)) = (w \ (f"x)))
15		imaeq2 4071	. . . . . . . . 9 |- ((w \ (f"y)) = (w \ (f"x)) -> (g"(w \ (f"y))) = (g"(w \ (f"x))))
16		sseq1 2470	. . . . . . . . 9 |- ((g"(w \ (f"y))) = (g"(w \ (f"x))) -> ((g"(w \ (f"y))) C_ (z \ y) <-> (g"(w \ (f"x))) C_ (z \ y)))
17	14, 15, 16	3syl 24	. . . . . . . 8 |- (y = x -> ((g"(w \ (f"y))) C_ (z \ y) <-> (g"(w \ (f"x))) C_ (z \ y)))
18		difeq2 2551	. . . . . . . . 9 |- (y = x -> (z \ y) = (z \ x))
19	18	sseq2d 2478	. . . . . . . 8 |- (y = x -> ((g"(w \ (f"x))) C_ (z \ y) <-> (g"(w \ (f"x))) C_ (z \ x)))
20	17, 19	bitrd 584	. . . . . . 7 |- (y = x -> ((g"(w \ (f"y))) C_ (z \ y) <-> (g"(w \ (f"x))) C_ (z \ x)))
21	12, 20	anbi12d 687	. . . . . 6 |- (y = x -> ((y C_ z /\ (g"(w \ (f"y))) C_ (z \ y)) <-> (x C_ z /\ (g"(w \ (f"x))) C_ (z \ x))))
22	21	cbvabv 2253	. . . . 5 |- {y | (y C_ z /\ (g"(w \ (f"y))) C_ (z \ y))} = {x | (x C_ z /\ (g"(w \ (f"x))) C_ (z \ x))}
23		eqid 1721	. . . . 5 |- ((f |` U.{y | (y C_ z /\ (g"(w \ (f"y))) C_ (z \ y))}) u. (`'g |` (z \ U.{y | (y C_ z /\ (g"(w \ (f"y))) C_ (z \ y))}))) = ((f |` U.{y | (y C_ z /\ (g"(w \ (f"y))) C_ (z \ y))}) u. (`'g |` (z \ U.{y | (y C_ z /\ (g"(w \ (f"y))) C_ (z \ y))})))
24		visset 2128	. . . . 5 |- w e. _V
25	11, 22, 23, 24	sbthlem10 5330	. . . 4 |- ((z ~<_ w /\ w ~<_ z) -> z ~~ w)
26	5, 10, 25	vtocl2g 2182	. . 3 |- ((A e. _V /\ B e. _V) -> ((A ~<_ B /\ B ~<_ A) -> A ~~ B))
27		reldom 5243	. . . 4 |- Rel ~<_
28	27	brrelexi 3840	. . 3 |- (A ~<_ B -> A e. _V)
29	27	brrelexi 3840	. . 3 |- (B ~<_ A -> B e. _V)
30	26, 28, 29	syl2an 501	. 2 |- ((A ~<_ B /\ B ~<_ A) -> ((A ~<_ B /\ B ~<_ A) -> A ~~ B))
31	30	pm2.43i 78	1 |- ((A ~<_ B /\ B ~<_ A) -> A ~~ B)

Syntax hints:   -> wi 3   <-> wb 162   /\ wa 239   = wceq 1136   e. wcel 1138  {cab 1708  _Vcvv 2125   \ cdif 2423   u. cun 2424   C_ wss 2426  U.cuni 2999   class class class wbr 3158  `'ccnv 3796   |` cres 3799  "cima 3800   ~~ cen 5234   ~<_ cdom 5235

This theorem is referenced by:  sbthbg 5332  sdomnsym 5336  sdomdomtr 5343  domtriord 5357  limenpsi 5409  php 5417  onomeneq 5422  unbnn 5447  omsubsdom 5677  omsubdom 5678  omsubel 5679  xpnnen 8563  znnen 8566  qnnen 8567  infxpidmlem1 8616  infxpidmlem12 8627  infunabs 8629  infcdaabs 8630  infdif 8632  infxpabs 8634  infmap1 8637  infmap2 8645  sndw 14158  dmsdtriordOLD 15042  omsubsdomOLD 15072  omsubdomOLD 15073  omsubelOLD 15074  ufilen 15261

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1142  ax-gen 1143  ax-8 1144  ax-9 1145  ax-10 1146  ax-11 1147  ax-12 1148  ax-13 1149  ax-14 1150  ax-17 1155  ax-4 1157  ax-5o 1159  ax-6o 1162  ax-9o 1319  ax-10o 1338  ax-16 1418  ax-11o 1426  ax-ext 1702  ax-rep 3243  ax-sep 3253  ax-nul 3260  ax-pow 3296  ax-pr 3339  ax-un 3601

This theorem depends on definitions:  df-bi 163  df-or 240  df-an 241  df-3an 857  df-ex 1165  df-sb 1374  df-eu 1613  df-mo 1614  df-clab 1709  df-cleq 1714  df-clel 1717  df-ne 1856  df-ral 1943  df-rex 1944  df-rab 1946  df-v 2127  df-dif 2430  df-un 2433  df-in 2436  df-ss 2438  df-nul 2702  df-pw 2859  df-sn 2873  df-pr 2874  df-op 2877  df-uni 3000  df-br 3159  df-opab 3214  df-id 3401  df-xp 3811  df-rel 3812  df-cnv 3813  df-co 3814  df-dm 3815  df-rn 3816  df-res 3817  df-ima 3818  df-fun 3819  df-fn 3820  df-f 3821  df-f1 3822  df-fo 3823  df-f1o 3824  df-en 5238  df-dom 5239

Copyright terms: Public domain