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 ‘ 𝐴 ) ↔ Lim ( card ‘ 𝐴 ) )

Proof

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