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 syl5bir ⊢ 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 ∈ On card ⁡ 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 ∈ On card ⁡ A = suc ⁡ x ∨ Lim ⁡ card ⁡ A
34 32 33 mpbi ⊢ card ⁡ A = ∅ ∨ ∃ x ∈ On card ⁡ A = suc ⁡ x ∨ Lim ⁡ card ⁡ A
35 3orass ⊢ card ⁡ A = ∅ ∨ ∃ x ∈ On card ⁡ A = suc ⁡ x ∨ Lim ⁡ card ⁡ A ↔ card ⁡ A = ∅ ∨ ∃ x ∈ On card ⁡ A = suc ⁡ x ∨ Lim ⁡ card ⁡ A
36 34 35 mpbi ⊢ card ⁡ A = ∅ ∨ ∃ x ∈ On card ⁡ A = suc ⁡ x ∨ Lim ⁡ card ⁡ A
37 36 ori ⊢ ¬ card ⁡ A = ∅ → ∃ x ∈ On card ⁡ A = suc ⁡ x ∨ Lim ⁡ card ⁡ A
38 29 30 37 3syl ⊢ ω ⊆ card ⁡ A → ∃ x ∈ On card ⁡ A = suc ⁡ x ∨ Lim ⁡ card ⁡ A
39 38 ord ⊢ ω ⊆ card ⁡ A → ¬ ∃ x ∈ On card ⁡ 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