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 ⊢ω⊆card⁡A↔Lim⁡card⁡A

Proof

Step Hyp Ref Expression
1 sseq2 ⊢card⁡A=suc⁡x→ω⊆card⁡A↔ω⊆suc⁡x
2 1 biimpd ⊢card⁡A=suc⁡x→ω⊆card⁡A→ω⊆suc⁡x
3 limom ⊢Lim⁡ω
4 limsssuc ⊢Lim⁡ω→ω⊆x↔ω⊆suc⁡x
5 3 4 ax-mp ⊢ω⊆x↔ω⊆suc⁡x
6 infensuc ⊢x∈On∧ω⊆x→x≈suc⁡x
7 6 ex ⊢x∈On→ω⊆x→x≈suc⁡x
8 5 7 biimtrrid ⊢x∈On→ω⊆suc⁡x→x≈suc⁡x
9 2 8 sylan9r ⊢x∈On∧card⁡A=suc⁡x→ω⊆card⁡A→x≈suc⁡x
10 breq2 ⊢card⁡A=suc⁡x→x≈card⁡A↔x≈suc⁡x
11 10 adantl ⊢x∈On∧card⁡A=suc⁡x→x≈card⁡A↔x≈suc⁡x
12 9 11 sylibrd ⊢x∈On∧card⁡A=suc⁡x→ω⊆card⁡A→x≈card⁡A
13 12 ex ⊢x∈On→card⁡A=suc⁡x→ω⊆card⁡A→x≈card⁡A
14 13 com3r ⊢ω⊆card⁡A→x∈On→card⁡A=suc⁡x→x≈card⁡A
15 14 imp ⊢ω⊆card⁡A∧x∈On→card⁡A=suc⁡x→x≈card⁡A
16 vex ⊢x∈V
17 16 sucid ⊢x∈suc⁡x
18 eleq2 ⊢card⁡A=suc⁡x→x∈card⁡A↔x∈suc⁡x
19 17 18 mpbiri ⊢card⁡A=suc⁡x→x∈card⁡A
20 cardidm ⊢card⁡card⁡A=card⁡A
21 19 20 eleqtrrdi ⊢card⁡A=suc⁡x→x∈card⁡card⁡A
22 cardne ⊢x∈card⁡card⁡A→¬x≈card⁡A
23 21 22 syl ⊢card⁡A=suc⁡x→¬x≈card⁡A
24 23 a1i ⊢ω⊆card⁡A∧x∈On→card⁡A=suc⁡x→¬x≈card⁡A
25 15 24 pm2.65d ⊢ω⊆card⁡A∧x∈On→¬card⁡A=suc⁡x
26 25 nrexdv ⊢ω⊆card⁡A→¬∃x∈Oncard⁡A=suc⁡x
27 peano1 ⊢∅∈ω
28 ssel ⊢ω⊆card⁡A→∅∈ω→∅∈card⁡A
29 27 28 mpi ⊢ω⊆card⁡A→∅∈card⁡A
30 n0i ⊢∅∈card⁡A→¬card⁡A=∅
31 cardon ⊢card⁡A∈On
32 31 onordi ⊢Ord⁡card⁡A
33 ordzsl ⊢Ord⁡card⁡A↔card⁡A=∅∨∃x∈Oncard⁡A=suc⁡x∨Lim⁡card⁡A
34 32 33 mpbi ⊢card⁡A=∅∨∃x∈Oncard⁡A=suc⁡x∨Lim⁡card⁡A
35 3orass ⊢card⁡A=∅∨∃x∈Oncard⁡A=suc⁡x∨Lim⁡card⁡A↔card⁡A=∅∨∃x∈Oncard⁡A=suc⁡x∨Lim⁡card⁡A
36 34 35 mpbi ⊢card⁡A=∅∨∃x∈Oncard⁡A=suc⁡x∨Lim⁡card⁡A
37 36 ori ⊢¬card⁡A=∅→∃x∈Oncard⁡A=suc⁡x∨Lim⁡card⁡A
38 29 30 37 3syl ⊢ω⊆card⁡A→∃x∈Oncard⁡A=suc⁡x∨Lim⁡card⁡A
39 38 ord ⊢ω⊆card⁡A→¬∃x∈Oncard⁡A=suc⁡x→Lim⁡card⁡A
40 26 39 mpd ⊢ω⊆card⁡A→Lim⁡card⁡A
41 limomss ⊢Lim⁡card⁡A→ω⊆card⁡A
42 40 41 impbii ⊢ω⊆card⁡A↔Lim⁡card⁡A