Metamath Proof Explorer

Theorem infensuc

Description: Any infinite ordinal is equinumerous to its successor. Exercise 7 of TakeutiZaring p. 88. Proved without the Axiom of Infinity. (Contributed by NM, 30-Oct-2003) (Revised by Mario Carneiro, 13-Jan-2013)

Ref Expression
Assertion infensuc 
|- ( ( A e. On /\ _om C_ A ) -> A ~~ suc A )

Proof

Step Hyp Ref Expression
1 onprc 
 |-  -. On e. _V
2 eleq1 
 |-  ( _om = On -> ( _om e. _V <-> On e. _V ) )
3 1 2 mtbiri 
 |-  ( _om = On -> -. _om e. _V )
4 ssexg 
 |-  ( ( _om C_ A /\ A e. On ) -> _om e. _V )
5 4 ancoms 
 |-  ( ( A e. On /\ _om C_ A ) -> _om e. _V )
6 3 5 nsyl3 
 |-  ( ( A e. On /\ _om C_ A ) -> -. _om = On )
7 omon 
 |-  ( _om e. On \/ _om = On )
8 7 ori 
 |-  ( -. _om e. On -> _om = On )
9 6 8 nsyl2 
 |-  ( ( A e. On /\ _om C_ A ) -> _om e. On )
10 id 
 |-  ( x = _om -> x = _om )
11 suceq 
 |-  ( x = _om -> suc x = suc _om )
12 10 11 breq12d 
 |-  ( x = _om -> ( x ~~ suc x <-> _om ~~ suc _om ) )
13 id 
 |-  ( x = y -> x = y )
14 suceq 
 |-  ( x = y -> suc x = suc y )
15 13 14 breq12d 
 |-  ( x = y -> ( x ~~ suc x <-> y ~~ suc y ) )
16 id 
 |-  ( x = suc y -> x = suc y )
17 suceq 
 |-  ( x = suc y -> suc x = suc suc y )
18 16 17 breq12d 
 |-  ( x = suc y -> ( x ~~ suc x <-> suc y ~~ suc suc y ) )
19 id 
 |-  ( x = A -> x = A )
20 suceq 
 |-  ( x = A -> suc x = suc A )
21 19 20 breq12d 
 |-  ( x = A -> ( x ~~ suc x <-> A ~~ suc A ) )
22 limom 
 |-  Lim _om
23 22 limensuci 
 |-  ( _om e. On -> _om ~~ suc _om )
24 vex 
 |-  y e. _V
25 24 sucex 
 |-  suc y e. _V
26 en2sn 
 |-  ( ( y e. _V /\ suc y e. _V ) -> { y } ~~ { suc y } )
27 24 25 26 mp2an 
 |-  { y } ~~ { suc y }
28 eloni 
 |-  ( y e. On -> Ord y )
29 ordirr 
 |-  ( Ord y -> -. y e. y )
30 28 29 syl 
 |-  ( y e. On -> -. y e. y )
31 disjsn 
 |-  ( ( y i^i { y } ) = (/) <-> -. y e. y )
32 30 31 sylibr 
 |-  ( y e. On -> ( y i^i { y } ) = (/) )
33 eloni 
 |-  ( suc y e. On -> Ord suc y )
34 ordirr 
 |-  ( Ord suc y -> -. suc y e. suc y )
35 33 34 syl 
 |-  ( suc y e. On -> -. suc y e. suc y )
36 sucelon 
 |-  ( y e. On <-> suc y e. On )
37 disjsn 
 |-  ( ( suc y i^i { suc y } ) = (/) <-> -. suc y e. suc y )
38 35 36 37 3imtr4i 
 |-  ( y e. On -> ( suc y i^i { suc y } ) = (/) )
39 32 38 jca 
 |-  ( y e. On -> ( ( y i^i { y } ) = (/) /\ ( suc y i^i { suc y } ) = (/) ) )
40 unen 
 |-  ( ( ( y ~~ suc y /\ { y } ~~ { suc y } ) /\ ( ( y i^i { y } ) = (/) /\ ( suc y i^i { suc y } ) = (/) ) ) -> ( y u. { y } ) ~~ ( suc y u. { suc y } ) )
41 df-suc 
 |-  suc y = ( y u. { y } )
42 df-suc 
 |-  suc suc y = ( suc y u. { suc y } )
43 40 41 42 3brtr4g 
 |-  ( ( ( y ~~ suc y /\ { y } ~~ { suc y } ) /\ ( ( y i^i { y } ) = (/) /\ ( suc y i^i { suc y } ) = (/) ) ) -> suc y ~~ suc suc y )
44 43 ex 
 |-  ( ( y ~~ suc y /\ { y } ~~ { suc y } ) -> ( ( ( y i^i { y } ) = (/) /\ ( suc y i^i { suc y } ) = (/) ) -> suc y ~~ suc suc y ) )
45 39 44 syl5 
 |-  ( ( y ~~ suc y /\ { y } ~~ { suc y } ) -> ( y e. On -> suc y ~~ suc suc y ) )
46 27 45 mpan2 
 |-  ( y ~~ suc y -> ( y e. On -> suc y ~~ suc suc y ) )
47 46 com12 
 |-  ( y e. On -> ( y ~~ suc y -> suc y ~~ suc suc y ) )
48 47 ad2antrr 
 |-  ( ( ( y e. On /\ _om e. On ) /\ _om C_ y ) -> ( y ~~ suc y -> suc y ~~ suc suc y ) )
49 vex 
 |-  x e. _V
50 limensuc 
 |-  ( ( x e. _V /\ Lim x ) -> x ~~ suc x )
51 49 50 mpan 
 |-  ( Lim x -> x ~~ suc x )
52 51 ad2antrr 
 |-  ( ( ( Lim x /\ _om e. On ) /\ _om C_ x ) -> x ~~ suc x )
53 52 a1d 
 |-  ( ( ( Lim x /\ _om e. On ) /\ _om C_ x ) -> ( A. y e. x ( _om C_ y -> y ~~ suc y ) -> x ~~ suc x ) )
54 12 15 18 21 23 48 53 tfindsg 
 |-  ( ( ( A e. On /\ _om e. On ) /\ _om C_ A ) -> A ~~ suc A )
55 54 exp31 
 |-  ( A e. On -> ( _om e. On -> ( _om C_ A -> A ~~ suc A ) ) )
56 55 com23 
 |-  ( A e. On -> ( _om C_ A -> ( _om e. On -> A ~~ suc A ) ) )
57 56 imp 
 |-  ( ( A e. On /\ _om C_ A ) -> ( _om e. On -> A ~~ suc A ) )
58 9 57 mpd 
 |-  ( ( A e. On /\ _om C_ A ) -> A ~~ suc A )