MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbth Unicode version

Theorem sbth 6949
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 6939 through sbthlem10 6948; this final piece mainly changes bound variables to eliminate the hypotheses of sbthlem10 6948. 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. (Contributed by NM, 8-Jun-1998.)
Assertion
Ref Expression
sbth  |-  ( ( A  ~<_  B  /\  B  ~<_  A )  ->  A  ~~  B )

Proof of Theorem sbth
StepHypRef Expression
1 reldom 6837 . . . 4  |-  Rel  ~<_
21brrelexi 4717 . . 3  |-  ( A  ~<_  B  ->  A  e.  _V )
31brrelexi 4717 . . 3  |-  ( B  ~<_  A  ->  B  e.  _V )
4 breq1 4000 . . . . . 6  |-  ( z  =  A  ->  (
z  ~<_  w  <->  A  ~<_  w ) )
5 breq2 4001 . . . . . 6  |-  ( z  =  A  ->  (
w  ~<_  z  <->  w  ~<_  A ) )
64, 5anbi12d 694 . . . . 5  |-  ( z  =  A  ->  (
( z  ~<_  w  /\  w  ~<_  z )  <->  ( A  ~<_  w  /\  w  ~<_  A ) ) )
7 breq1 4000 . . . . 5  |-  ( z  =  A  ->  (
z  ~~  w  <->  A  ~~  w ) )
86, 7imbi12d 313 . . . 4  |-  ( z  =  A  ->  (
( ( z  ~<_  w  /\  w  ~<_  z )  ->  z  ~~  w
)  <->  ( ( A  ~<_  w  /\  w  ~<_  A )  ->  A  ~~  w ) ) )
9 breq2 4001 . . . . . 6  |-  ( w  =  B  ->  ( A  ~<_  w  <->  A  ~<_  B ) )
10 breq1 4000 . . . . . 6  |-  ( w  =  B  ->  (
w  ~<_  A  <->  B  ~<_  A ) )
119, 10anbi12d 694 . . . . 5  |-  ( w  =  B  ->  (
( A  ~<_  w  /\  w  ~<_  A )  <->  ( A  ~<_  B  /\  B  ~<_  A ) ) )
12 breq2 4001 . . . . 5  |-  ( w  =  B  ->  ( A  ~~  w  <->  A  ~~  B ) )
1311, 12imbi12d 313 . . . 4  |-  ( w  =  B  ->  (
( ( A  ~<_  w  /\  w  ~<_  A )  ->  A  ~~  w
)  <->  ( ( A  ~<_  B  /\  B  ~<_  A )  ->  A  ~~  B ) ) )
14 vex 2766 . . . . 5  |-  z  e. 
_V
15 sseq1 3174 . . . . . . 7  |-  ( y  =  x  ->  (
y  C_  z  <->  x  C_  z
) )
16 imaeq2 4996 . . . . . . . . . 10  |-  ( y  =  x  ->  (
f " y )  =  ( f "
x ) )
1716difeq2d 3269 . . . . . . . . 9  |-  ( y  =  x  ->  (
w  \  ( f " y ) )  =  ( w  \ 
( f " x
) ) )
1817imaeq2d 5000 . . . . . . . 8  |-  ( y  =  x  ->  (
g " ( w 
\  ( f "
y ) ) )  =  ( g "
( w  \  (
f " x ) ) ) )
19 difeq2 3263 . . . . . . . 8  |-  ( y  =  x  ->  (
z  \  y )  =  ( z  \  x ) )
2018, 19sseq12d 3182 . . . . . . 7  |-  ( y  =  x  ->  (
( g " (
w  \  ( f " y ) ) )  C_  ( z  \  y )  <->  ( g " ( w  \ 
( f " x
) ) )  C_  ( z  \  x
) ) )
2115, 20anbi12d 694 . . . . . 6  |-  ( y  =  x  ->  (
( y  C_  z  /\  ( g " (
w  \  ( f " y ) ) )  C_  ( z  \  y ) )  <-> 
( x  C_  z  /\  ( g " (
w  \  ( f " x ) ) )  C_  ( z  \  x ) ) ) )
2221cbvabv 2377 . . . . 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 2258 . . . . 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 vex 2766 . . . . 5  |-  w  e. 
_V
2514, 22, 23, 24sbthlem10 6948 . . . 4  |-  ( ( z  ~<_  w  /\  w  ~<_  z )  ->  z  ~~  w )
268, 13, 25vtocl2g 2822 . . 3  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( ( A  ~<_  B  /\  B  ~<_  A )  ->  A  ~~  B
) )
272, 3, 26syl2an 465 . 2  |-  ( ( A  ~<_  B  /\  B  ~<_  A )  ->  (
( A  ~<_  B  /\  B  ~<_  A )  ->  A  ~~  B ) )
2827pm2.43i 45 1  |-  ( ( A  ~<_  B  /\  B  ~<_  A )  ->  A  ~~  B )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    = wceq 1619    e. wcel 1621   {cab 2244   _Vcvv 2763    \ cdif 3124    u. cun 3125    C_ wss 3127   U.cuni 3801   class class class wbr 3997   `'ccnv 4660    |` cres 4663   "cima 4664    ~~ cen 6828    ~<_ cdom 6829
This theorem is referenced by:  sbthb  6950  sdomnsym  6954  domtriord  6975  xpen  6992  limenpsi  7004  php  7013  onomeneq  7018  unbnn  7081  infxpenlem  7609  fseqen  7622  infpwfien  7657  inffien  7658  alephdom  7676  mappwen  7707  infcdaabs  7800  infunabs  7801  infcda  7802  infdif  7803  infxpabs  7806  infmap2  7812  gchhar  8261  gchaleph  8265  inttsk  8364  inar1  8365  xpnnenOLD  12450  znnen  12453  qnnen  12454  rpnnen  12467  rexpen  12468  mreexfidimd  13514  acsinfdimd  14247  fislw  14898  opnreen  18298  ovolctb2  18813  vitali  18930  aannenlem3  19672  basellem4  20283  lgsqrlem4  20545  umgraex  23247  sndw  24466  pellexlem4  26284  pellexlem5  26285  idomsubgmo  26881
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239  ax-sep 4115  ax-nul 4123  ax-pow 4160  ax-pr 4186  ax-un 4484
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2122  df-mo 2123  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-ral 2523  df-rex 2524  df-rab 2527  df-v 2765  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-nul 3431  df-if 3540  df-pw 3601  df-sn 3620  df-pr 3621  df-op 3623  df-uni 3802  df-br 3998  df-opab 4052  df-id 4281  df-xp 4675  df-rel 4676  df-cnv 4677  df-co 4678  df-dm 4679  df-rn 4680  df-res 4681  df-ima 4682  df-fun 4683  df-fn 4684  df-f 4685  df-f1 4686  df-fo 4687  df-f1o 4688  df-en 6832  df-dom 6833
  Copyright terms: Public domain W3C validator