Metamath Proof Explorer

Theorem cardlim

Description: An infinite cardinal is a limit ordinal. Equivalent to Exercise 4 of TakeutiZaring p. 91. (Contributed by Mario Carneiro, 13-Jan-2013)

Ref Expression
Assertion cardlim 
|- ( _om C_ ( card ` A ) <-> Lim ( card ` A ) )

Proof

Step Hyp Ref Expression
1 sseq2 
 |-  ( ( card ` A ) = suc x -> ( _om C_ ( card ` A ) <-> _om C_ suc x ) )
2 1 biimpd 
 |-  ( ( card ` A ) = suc x -> ( _om C_ ( card ` A ) -> _om C_ suc x ) )
3 limom 
 |-  Lim _om
4 limsssuc 
 |-  ( Lim _om -> ( _om C_ x <-> _om C_ suc x ) )
5 3 4 ax-mp 
 |-  ( _om C_ x <-> _om C_ suc x )
6 infensuc 
 |-  ( ( x e. On /\ _om C_ x ) -> x ~~ suc x )
7 6 ex 
 |-  ( x e. On -> ( _om C_ x -> x ~~ suc x ) )
8 5 7 syl5bir 
 |-  ( x e. On -> ( _om C_ suc x -> x ~~ suc x ) )
9 2 8 sylan9r 
 |-  ( ( x e. On /\ ( card ` A ) = suc x ) -> ( _om C_ ( card ` A ) -> x ~~ suc x ) )
10 breq2 
 |-  ( ( card ` A ) = suc x -> ( x ~~ ( card ` A ) <-> x ~~ suc x ) )
11 10 adantl 
 |-  ( ( x e. On /\ ( card ` A ) = suc x ) -> ( x ~~ ( card ` A ) <-> x ~~ suc x ) )
12 9 11 sylibrd 
 |-  ( ( x e. On /\ ( card ` A ) = suc x ) -> ( _om C_ ( card ` A ) -> x ~~ ( card ` A ) ) )
13 12 ex 
 |-  ( x e. On -> ( ( card ` A ) = suc x -> ( _om C_ ( card ` A ) -> x ~~ ( card ` A ) ) ) )
14 13 com3r 
 |-  ( _om C_ ( card ` A ) -> ( x e. On -> ( ( card ` A ) = suc x -> x ~~ ( card ` A ) ) ) )
15 14 imp 
 |-  ( ( _om C_ ( card ` A ) /\ x e. On ) -> ( ( card ` A ) = suc x -> x ~~ ( card ` A ) ) )
16 vex 
 |-  x e. _V
17 16 sucid 
 |-  x e. suc x
18 eleq2 
 |-  ( ( card ` A ) = suc x -> ( x e. ( card ` A ) <-> x e. suc x ) )
19 17 18 mpbiri 
 |-  ( ( card ` A ) = suc x -> x e. ( card ` A ) )
20 cardidm 
 |-  ( card ` ( card ` A ) ) = ( card ` A )
21 19 20 eleqtrrdi 
 |-  ( ( card ` A ) = suc x -> x e. ( card ` ( card ` A ) ) )
22 cardne 
 |-  ( x e. ( card ` ( card ` A ) ) -> -. x ~~ ( card ` A ) )
23 21 22 syl 
 |-  ( ( card ` A ) = suc x -> -. x ~~ ( card ` A ) )
24 23 a1i 
 |-  ( ( _om C_ ( card ` A ) /\ x e. On ) -> ( ( card ` A ) = suc x -> -. x ~~ ( card ` A ) ) )
25 15 24 pm2.65d 
 |-  ( ( _om C_ ( card ` A ) /\ x e. On ) -> -. ( card ` A ) = suc x )
26 25 nrexdv 
 |-  ( _om C_ ( card ` A ) -> -. E. x e. On ( card ` A ) = suc x )
27 peano1 
 |-  (/) e. _om
28 ssel 
 |-  ( _om C_ ( card ` A ) -> ( (/) e. _om -> (/) e. ( card ` A ) ) )
29 27 28 mpi 
 |-  ( _om C_ ( card ` A ) -> (/) e. ( card ` A ) )
30 n0i 
 |-  ( (/) e. ( card ` A ) -> -. ( card ` A ) = (/) )
31 cardon 
 |-  ( card ` A ) e. On
32 31 onordi 
 |-  Ord ( card ` A )
33 ordzsl 
 |-  ( Ord ( card ` A ) <-> ( ( card ` A ) = (/) \/ E. x e. On ( card ` A ) = suc x \/ Lim ( card ` A ) ) )
34 32 33 mpbi 
 |-  ( ( card ` A ) = (/) \/ E. x e. On ( card ` A ) = suc x \/ Lim ( card ` A ) )
35 3orass 
 |-  ( ( ( card ` A ) = (/) \/ E. x e. On ( card ` A ) = suc x \/ Lim ( card ` A ) ) <-> ( ( card ` A ) = (/) \/ ( E. x e. On ( card ` A ) = suc x \/ Lim ( card ` A ) ) ) )
36 34 35 mpbi 
 |-  ( ( card ` A ) = (/) \/ ( E. x e. On ( card ` A ) = suc x \/ Lim ( card ` A ) ) )
37 36 ori 
 |-  ( -. ( card ` A ) = (/) -> ( E. x e. On ( card ` A ) = suc x \/ Lim ( card ` A ) ) )
38 29 30 37 3syl 
 |-  ( _om C_ ( card ` A ) -> ( E. x e. On ( card ` A ) = suc x \/ Lim ( card ` A ) ) )
39 38 ord 
 |-  ( _om C_ ( card ` A ) -> ( -. E. x e. On ( card ` A ) = suc x -> Lim ( card ` A ) ) )
40 26 39 mpd 
 |-  ( _om C_ ( card ` A ) -> Lim ( card ` A ) )
41 limomss 
 |-  ( Lim ( card ` A ) -> _om C_ ( card ` A ) )
42 40 41 impbii 
 |-  ( _om C_ ( card ` A ) <-> Lim ( card ` A ) )