Theorem sbth 4391

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 4381 through sbthlem10 4390; this final piece mainly changes bound variables to eliminate the hypotheses of sbthlem10 4390. 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 2590	. . . . . 6 |- (z = A -> (z ~<_ w <-> A ~<_ w))
2		breq2 2591	. . . . . 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 2590	. . . . 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 2591	. . . . . 6 |- (w = B -> (A ~<_ w <-> A ~<_ B))
7		breq1 2590	. . . . . 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 2591	. . . . 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 1788	. . . . 5 |- z e. V
12		sseq1 2053	. . . . . . 7 |- (y = x -> (y (_ z <-> x (_ z))
13		imaeq2 3353	. . . . . . . . . 10 |- (y = x -> (f"y) = (f"x))
14	13	difeq2d 2130	. . . . . . . . 9 |- (y = x -> (w \ (f"y)) = (w \ (f"x)))
15		imaeq2 3353	. . . . . . . . 9 |- ((w \ (f"y)) = (w \ (f"x)) -> (g"(w \ (f"y))) = (g"(w \ (f"x))))
16		sseq1 2053	. . . . . . . . 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 2125	. . . . . . . . 9 |- (y = x -> (z \ y) = (z \ x))
19	18	sseq2d 2060	. . . . . . . 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 1881	. . . . 5 |- {y | (y (_ z /\ (g"(w \ (f"y))) (_ (z \ y))} = {x | (x (_ z /\ (g"(w \ (f"x))) (_ (z \ x))}
23		eqid 1452	. . . . 5 |- ((f |` U.{y | (y (_ z /\ (g"(w \ (f"y))) (_ (z \ y))}) u. (`'g |` (z \ U.{y | (y (_ z /\ (g"(w \ (f"y))) (_ (z \ y))}))) = ((f |` U.{y | (y (_ z /\ (g"(w \ (f"y))) (_ (z \ y))}) u. (`'g |` (z \ U.{y | (y (_ z /\ (g"(w \ (f"y))) (_ (z \ y))})))
24		visset 1788	. . . . 5 |- w e. V
25	11, 22, 23, 24	sbthlem10 4390	. . . 4 |- ((z ~<_ w /\ w ~<_ z) -> z ~~ w)
26	5, 10, 25	vtocl2g 1825	. . 3 |- ((A e. V /\ B e. V) -> ((A ~<_ B /\ B ~<_ A) -> A ~~ B))
27		reldom 4309	. . . 4 |- Rel ~<_
28	27	brrelexi 3170	. . 3 |- (A ~<_ B -> A e. V)
29	27	brrelexi 3170	. . 3 |- (B ~<_ A -> B e. 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)

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 1099   e. wcel 1105  {cab 1440  Vcvv 1786   \ cdif 2015   u. cun 2016   (_ wss 2018  U.cuni 2471   class class class wbr 2587  `'ccnv 3132   |` cres 3135  "cima 3136   ~~ cen 4302   ~<_ cdom 4303

This theorem is referenced by:  sbthbg 4392  sdomnsym 4396  sdomdomtr 4403  limenpsi 4437  php 4445  onomeneq 4450  unbnn 4473  xpnnen 7392  znnen 7396  qnnen 7397  infxpidmlem1 7446  infxpidmlem12 7457  infunabs 7459  infcdaabs 7460  infdif 7462  infxpabs 7464  infmap1 7467  infmap2 7474

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-rep 2661  ax-sep 2671  ax-nul 2678  ax-pow 2710  ax-pr 2747  ax-un 2830

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 774  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-ral 1625  df-rex 1626  df-v 1787  df-dif 2020  df-un 2021  df-in 2022  df-ss 2024  df-nul 2252  df-pw 2373  df-sn 2383  df-pr 2384  df-op 2387  df-uni 2472  df-br 2588  df-opab 2635  df-id 2797  df-xp 3147  df-rel 3148  df-cnv 3149  df-co 3150  df-dm 3151  df-rn 3152  df-res 3153  df-ima 3154  df-fun 3155  df-fn 3156  df-f 3157  df-f1 3158  df-fo 3159  df-f1o 3160  df-en 4305  df-dom 4306

Copyright terms: Public domain