Theorem isbth 7028

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 7018 through sbthlemi10 7027; this final piece mainly changes bound variables to eliminate the hypotheses of sbthlemi10 7027. 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. The proof does require the law of the excluded middle which cannot be avoided as shown at exmidsbthr 15583. (Contributed by NM, 8-Jun-1998.)

Assertion

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

Proof of Theorem isbth

Dummy variables x y z w f g are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simprl 529	. 2 |- ( (EXMID /\ ( A ~<_ B /\ B ~<_ A ) ) -> A ~<_ B )
2		simprr 531	. 2 |- ( (EXMID /\ ( A ~<_ B /\ B ~<_ A ) ) -> B ~<_ A )
3		reldom 6801	. . . . 5 |- Rel ~<_
4	3	brrelex1i 4703	. . . 4 |- ( B ~<_ A -> B e. _V )
5	2, 4	syl 14	. . 3 |- ( (EXMID /\ ( A ~<_ B /\ B ~<_ A ) ) -> B e. _V )
6		breq2 4034	. . . . . 6 |- ( w = B -> ( A ~<_ w <-> A ~<_ B ) )
7		breq1 4033	. . . . . 6 |- ( w = B -> ( w ~<_ A <-> B ~<_ A ) )
8	6, 7	anbi12d 473	. . . . 5 |- ( w = B -> ( ( A ~<_ w /\ w ~<_ A ) <-> ( A ~<_ B /\ B ~<_ A ) ) )
9		breq2 4034	. . . . 5 |- ( w = B -> ( A ~~ w <-> A ~~ B ) )
10	8, 9	imbi12d 234	. . . 4 |- ( w = B -> ( ( ( A ~<_ w /\ w ~<_ A ) -> A ~~ w ) <-> ( ( A ~<_ B /\ B ~<_ A ) -> A ~~ B ) ) )
11	10	adantl 277	. . 3 |- ( ( (EXMID /\ ( A ~<_ B /\ B ~<_ A ) ) /\ w = B ) -> ( ( ( A ~<_ w /\ w ~<_ A ) -> A ~~ w ) <-> ( ( A ~<_ B /\ B ~<_ A ) -> A ~~ B ) ) )
12	3	brrelex1i 4703	. . . . 5 |- ( A ~<_ B -> A e. _V )
13	1, 12	syl 14	. . . 4 |- ( (EXMID /\ ( A ~<_ B /\ B ~<_ A ) ) -> A e. _V )
14		breq1 4033	. . . . . . 7 |- ( z = A -> ( z ~<_ w <-> A ~<_ w ) )
15		breq2 4034	. . . . . . 7 |- ( z = A -> ( w ~<_ z <-> w ~<_ A ) )
16	14, 15	anbi12d 473	. . . . . 6 |- ( z = A -> ( ( z ~<_ w /\ w ~<_ z ) <-> ( A ~<_ w /\ w ~<_ A ) ) )
17		breq1 4033	. . . . . 6 |- ( z = A -> ( z ~~ w <-> A ~~ w ) )
18	16, 17	imbi12d 234	. . . . 5 |- ( z = A -> ( ( ( z ~<_ w /\ w ~<_ z ) -> z ~~ w ) <-> ( ( A ~<_ w /\ w ~<_ A ) -> A ~~ w ) ) )
19	18	adantl 277	. . . 4 |- ( ( (EXMID /\ ( A ~<_ B /\ B ~<_ A ) ) /\ z = A ) -> ( ( ( z ~<_ w /\ w ~<_ z ) -> z ~~ w ) <-> ( ( A ~<_ w /\ w ~<_ A ) -> A ~~ w ) ) )
20		vex 2763	. . . . . . 7 |- z e. _V
21		sseq1 3203	. . . . . . . . 9 |- ( y = x -> ( y C_ z <-> x C_ z ) )
22		imaeq2 5002	. . . . . . . . . . . 12 |- ( y = x -> ( f " y ) = ( f " x ) )
23	22	difeq2d 3278	. . . . . . . . . . 11 |- ( y = x -> ( w \ ( f " y ) ) = ( w \ ( f " x ) ) )
24	23	imaeq2d 5006	. . . . . . . . . 10 |- ( y = x -> ( g " ( w \ ( f " y ) ) ) = ( g " ( w \ ( f " x ) ) ) )
25		difeq2 3272	. . . . . . . . . 10 |- ( y = x -> ( z \ y ) = ( z \ x ) )
26	24, 25	sseq12d 3211	. . . . . . . . 9 |- ( y = x -> ( ( g " ( w \ ( f " y ) ) ) C_ ( z \ y ) <-> ( g " ( w \ ( f " x ) ) ) C_ ( z \ x ) ) )
27	21, 26	anbi12d 473	. . . . . . . 8 |- ( y = x -> ( ( y C_ z /\ ( g " ( w \ ( f " y ) ) ) C_ ( z \ y ) ) <-> ( x C_ z /\ ( g " ( w \ ( f " x ) ) ) C_ ( z \ x ) ) ) )
28	27	cbvabv 2318	. . . . . . 7 |- { y | ( y C_ z /\ ( g " ( w \ ( f " y ) ) ) C_ ( z \ y ) ) } = { x | ( x C_ z /\ ( g " ( w \ ( f " x ) ) ) C_ ( z \ x ) ) }
29		eqid 2193	. . . . . . 7 |- ( ( 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 ) ) } ) ) )
30		vex 2763	. . . . . . 7 |- w e. _V
31	20, 28, 29, 30	sbthlemi10 7027	. . . . . 6 |- ( (EXMID /\ ( z ~<_ w /\ w ~<_ z ) ) -> z ~~ w )
32	31	ex 115	. . . . 5 |- (EXMID -> ( ( z ~<_ w /\ w ~<_ z ) -> z ~~ w ) )
33	32	adantr 276	. . . 4 |- ( (EXMID /\ ( A ~<_ B /\ B ~<_ A ) ) -> ( ( z ~<_ w /\ w ~<_ z ) -> z ~~ w ) )
34	13, 19, 33	vtocld 2813	. . 3 |- ( (EXMID /\ ( A ~<_ B /\ B ~<_ A ) ) -> ( ( A ~<_ w /\ w ~<_ A ) -> A ~~ w ) )
35	5, 11, 34	vtocld 2813	. 2 |- ( (EXMID /\ ( A ~<_ B /\ B ~<_ A ) ) -> ( ( A ~<_ B /\ B ~<_ A ) -> A ~~ B ) )
36	1, 2, 35	mp2and 433	1 |- ( (EXMID /\ ( A ~<_ B /\ B ~<_ A ) ) -> A ~~ B )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1364   e. wcel 2164   {cab 2179   _Vcvv 2760   \ cdif 3151   u. cun 3152   C_ wss 3154   U.cuni 3836   class class class wbr 4030  EXMIDwem 4224   `'ccnv 4659   |` cres 4662   "cima 4663   ~~ cen 6794   ~<_ cdom 6795

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4148  ax-nul 4156  ax-pow 4204  ax-pr 4239  ax-un 4465

This theorem depends on definitions:  df-bi 117  df-stab 832  df-dc 836  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-rab 2481  df-v 2762  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3448  df-pw 3604  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-br 4031  df-opab 4092  df-exmid 4225  df-id 4325  df-xp 4666  df-rel 4667  df-cnv 4668  df-co 4669  df-dm 4670  df-rn 4671  df-res 4672  df-ima 4673  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-en 6797  df-dom 6798

This theorem is referenced by:  exmidsbth  15584