ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  isbth Unicode version

Theorem isbth 6655
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 6645 through sbthlemi10 6654; this final piece mainly changes bound variables to eliminate the hypotheses of sbthlemi10 6654. 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 11570. (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.
StepHypRef Expression
1 simprl 498 . 2  |-  ( (EXMID  /\  ( A  ~<_  B  /\  B  ~<_  A ) )  ->  A  ~<_  B )
2 simprr 499 . 2  |-  ( (EXMID  /\  ( A  ~<_  B  /\  B  ~<_  A ) )  ->  B  ~<_  A )
3 reldom 6442 . . . . 5  |-  Rel  ~<_
43brrelexi 4468 . . . 4  |-  ( B  ~<_  A  ->  B  e.  _V )
52, 4syl 14 . . 3  |-  ( (EXMID  /\  ( A  ~<_  B  /\  B  ~<_  A ) )  ->  B  e.  _V )
6 breq2 3841 . . . . . 6  |-  ( w  =  B  ->  ( A  ~<_  w  <->  A  ~<_  B ) )
7 breq1 3840 . . . . . 6  |-  ( w  =  B  ->  (
w  ~<_  A  <->  B  ~<_  A ) )
86, 7anbi12d 457 . . . . 5  |-  ( w  =  B  ->  (
( A  ~<_  w  /\  w  ~<_  A )  <->  ( A  ~<_  B  /\  B  ~<_  A ) ) )
9 breq2 3841 . . . . 5  |-  ( w  =  B  ->  ( A  ~~  w  <->  A  ~~  B ) )
108, 9imbi12d 232 . . . 4  |-  ( w  =  B  ->  (
( ( A  ~<_  w  /\  w  ~<_  A )  ->  A  ~~  w
)  <->  ( ( A  ~<_  B  /\  B  ~<_  A )  ->  A  ~~  B ) ) )
1110adantl 271 . . 3  |-  ( ( (EXMID 
/\  ( A  ~<_  B  /\  B  ~<_  A ) )  /\  w  =  B )  ->  (
( ( A  ~<_  w  /\  w  ~<_  A )  ->  A  ~~  w
)  <->  ( ( A  ~<_  B  /\  B  ~<_  A )  ->  A  ~~  B ) ) )
123brrelexi 4468 . . . . 5  |-  ( A  ~<_  B  ->  A  e.  _V )
131, 12syl 14 . . . 4  |-  ( (EXMID  /\  ( A  ~<_  B  /\  B  ~<_  A ) )  ->  A  e.  _V )
14 breq1 3840 . . . . . . 7  |-  ( z  =  A  ->  (
z  ~<_  w  <->  A  ~<_  w ) )
15 breq2 3841 . . . . . . 7  |-  ( z  =  A  ->  (
w  ~<_  z  <->  w  ~<_  A ) )
1614, 15anbi12d 457 . . . . . 6  |-  ( z  =  A  ->  (
( z  ~<_  w  /\  w  ~<_  z )  <->  ( A  ~<_  w  /\  w  ~<_  A ) ) )
17 breq1 3840 . . . . . 6  |-  ( z  =  A  ->  (
z  ~~  w  <->  A  ~~  w ) )
1816, 17imbi12d 232 . . . . 5  |-  ( z  =  A  ->  (
( ( z  ~<_  w  /\  w  ~<_  z )  ->  z  ~~  w
)  <->  ( ( A  ~<_  w  /\  w  ~<_  A )  ->  A  ~~  w ) ) )
1918adantl 271 . . . 4  |-  ( ( (EXMID 
/\  ( A  ~<_  B  /\  B  ~<_  A ) )  /\  z  =  A )  ->  (
( ( z  ~<_  w  /\  w  ~<_  z )  ->  z  ~~  w
)  <->  ( ( A  ~<_  w  /\  w  ~<_  A )  ->  A  ~~  w ) ) )
20 vex 2622 . . . . . . 7  |-  z  e. 
_V
21 sseq1 3045 . . . . . . . . 9  |-  ( y  =  x  ->  (
y  C_  z  <->  x  C_  z
) )
22 imaeq2 4757 . . . . . . . . . . . 12  |-  ( y  =  x  ->  (
f " y )  =  ( f "
x ) )
2322difeq2d 3116 . . . . . . . . . . 11  |-  ( y  =  x  ->  (
w  \  ( f " y ) )  =  ( w  \ 
( f " x
) ) )
2423imaeq2d 4761 . . . . . . . . . 10  |-  ( y  =  x  ->  (
g " ( w 
\  ( f "
y ) ) )  =  ( g "
( w  \  (
f " x ) ) ) )
25 difeq2 3110 . . . . . . . . . 10  |-  ( y  =  x  ->  (
z  \  y )  =  ( z  \  x ) )
2624, 25sseq12d 3053 . . . . . . . . 9  |-  ( y  =  x  ->  (
( g " (
w  \  ( f " y ) ) )  C_  ( z  \  y )  <->  ( g " ( w  \ 
( f " x
) ) )  C_  ( z  \  x
) ) )
2721, 26anbi12d 457 . . . . . . . 8  |-  ( y  =  x  ->  (
( y  C_  z  /\  ( g " (
w  \  ( f " y ) ) )  C_  ( z  \  y ) )  <-> 
( x  C_  z  /\  ( g " (
w  \  ( f " x ) ) )  C_  ( z  \  x ) ) ) )
2827cbvabv 2211 . . . . . . 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 2088 . . . . . . 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 2622 . . . . . . 7  |-  w  e. 
_V
3120, 28, 29, 30sbthlemi10 6654 . . . . . 6  |-  ( (EXMID  /\  ( z  ~<_  w  /\  w  ~<_  z ) )  ->  z  ~~  w
)
3231ex 113 . . . . 5  |-  (EXMID  ->  (
( z  ~<_  w  /\  w  ~<_  z )  -> 
z  ~~  w )
)
3332adantr 270 . . . 4  |-  ( (EXMID  /\  ( A  ~<_  B  /\  B  ~<_  A ) )  ->  ( ( z  ~<_  w  /\  w  ~<_  z )  ->  z  ~~  w ) )
3413, 19, 33vtocld 2671 . . 3  |-  ( (EXMID  /\  ( A  ~<_  B  /\  B  ~<_  A ) )  ->  ( ( A  ~<_  w  /\  w  ~<_  A )  ->  A  ~~  w ) )
355, 11, 34vtocld 2671 . 2  |-  ( (EXMID  /\  ( A  ~<_  B  /\  B  ~<_  A ) )  ->  ( ( A  ~<_  B  /\  B  ~<_  A )  ->  A  ~~  B ) )
361, 2, 35mp2and 424 1  |-  ( (EXMID  /\  ( A  ~<_  B  /\  B  ~<_  A ) )  ->  A  ~~  B
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103    = wceq 1289    e. wcel 1438   {cab 2074   _Vcvv 2619    \ cdif 2994    u. cun 2995    C_ wss 2997   U.cuni 3648   class class class wbr 3837  EXMIDwem 4020   `'ccnv 4427    |` cres 4430   "cima 4431    ~~ cen 6435    ~<_ cdom 6436
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-13 1449  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3949  ax-nul 3957  ax-pow 4001  ax-pr 4027  ax-un 4251
This theorem depends on definitions:  df-bi 115  df-stab 776  df-dc 781  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-rex 2365  df-rab 2368  df-v 2621  df-dif 2999  df-un 3001  df-in 3003  df-ss 3010  df-nul 3285  df-pw 3427  df-sn 3447  df-pr 3448  df-op 3450  df-uni 3649  df-br 3838  df-opab 3892  df-exmid 4021  df-id 4111  df-xp 4434  df-rel 4435  df-cnv 4436  df-co 4437  df-dm 4438  df-rn 4439  df-res 4440  df-ima 4441  df-fun 5004  df-fn 5005  df-f 5006  df-f1 5007  df-fo 5008  df-f1o 5009  df-en 6438  df-dom 6439
This theorem is referenced by:  exmidsbth  11571
  Copyright terms: Public domain W3C validator