| Step | Hyp | Ref
| Expression |
| 1 | | sseq2 4010 |
. . . . . . . . . . 11
⊢
((card‘𝐴) =
suc 𝑥 → (ω
⊆ (card‘𝐴)
↔ ω ⊆ suc 𝑥)) |
| 2 | 1 | biimpd 229 |
. . . . . . . . . 10
⊢
((card‘𝐴) =
suc 𝑥 → (ω
⊆ (card‘𝐴)
→ ω ⊆ suc 𝑥)) |
| 3 | | limom 7903 |
. . . . . . . . . . . 12
⊢ Lim
ω |
| 4 | | limsssuc 7871 |
. . . . . . . . . . . 12
⊢ (Lim
ω → (ω ⊆ 𝑥 ↔ ω ⊆ suc 𝑥)) |
| 5 | 3, 4 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (ω
⊆ 𝑥 ↔ ω
⊆ suc 𝑥) |
| 6 | | infensuc 9195 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ On ∧ ω ⊆
𝑥) → 𝑥 ≈ suc 𝑥) |
| 7 | 6 | ex 412 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ On → (ω
⊆ 𝑥 → 𝑥 ≈ suc 𝑥)) |
| 8 | 5, 7 | biimtrrid 243 |
. . . . . . . . . 10
⊢ (𝑥 ∈ On → (ω
⊆ suc 𝑥 → 𝑥 ≈ suc 𝑥)) |
| 9 | 2, 8 | sylan9r 508 |
. . . . . . . . 9
⊢ ((𝑥 ∈ On ∧
(card‘𝐴) = suc 𝑥) → (ω ⊆
(card‘𝐴) → 𝑥 ≈ suc 𝑥)) |
| 10 | | breq2 5147 |
. . . . . . . . . 10
⊢
((card‘𝐴) =
suc 𝑥 → (𝑥 ≈ (card‘𝐴) ↔ 𝑥 ≈ suc 𝑥)) |
| 11 | 10 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑥 ∈ On ∧
(card‘𝐴) = suc 𝑥) → (𝑥 ≈ (card‘𝐴) ↔ 𝑥 ≈ suc 𝑥)) |
| 12 | 9, 11 | sylibrd 259 |
. . . . . . . 8
⊢ ((𝑥 ∈ On ∧
(card‘𝐴) = suc 𝑥) → (ω ⊆
(card‘𝐴) → 𝑥 ≈ (card‘𝐴))) |
| 13 | 12 | ex 412 |
. . . . . . 7
⊢ (𝑥 ∈ On →
((card‘𝐴) = suc 𝑥 → (ω ⊆
(card‘𝐴) → 𝑥 ≈ (card‘𝐴)))) |
| 14 | 13 | com3r 87 |
. . . . . 6
⊢ (ω
⊆ (card‘𝐴)
→ (𝑥 ∈ On →
((card‘𝐴) = suc 𝑥 → 𝑥 ≈ (card‘𝐴)))) |
| 15 | 14 | imp 406 |
. . . . 5
⊢ ((ω
⊆ (card‘𝐴)
∧ 𝑥 ∈ On) →
((card‘𝐴) = suc 𝑥 → 𝑥 ≈ (card‘𝐴))) |
| 16 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
| 17 | 16 | sucid 6466 |
. . . . . . . . 9
⊢ 𝑥 ∈ suc 𝑥 |
| 18 | | eleq2 2830 |
. . . . . . . . 9
⊢
((card‘𝐴) =
suc 𝑥 → (𝑥 ∈ (card‘𝐴) ↔ 𝑥 ∈ suc 𝑥)) |
| 19 | 17, 18 | mpbiri 258 |
. . . . . . . 8
⊢
((card‘𝐴) =
suc 𝑥 → 𝑥 ∈ (card‘𝐴)) |
| 20 | | cardidm 9999 |
. . . . . . . 8
⊢
(card‘(card‘𝐴)) = (card‘𝐴) |
| 21 | 19, 20 | eleqtrrdi 2852 |
. . . . . . 7
⊢
((card‘𝐴) =
suc 𝑥 → 𝑥 ∈
(card‘(card‘𝐴))) |
| 22 | | cardne 10005 |
. . . . . . 7
⊢ (𝑥 ∈
(card‘(card‘𝐴))
→ ¬ 𝑥 ≈
(card‘𝐴)) |
| 23 | 21, 22 | syl 17 |
. . . . . 6
⊢
((card‘𝐴) =
suc 𝑥 → ¬ 𝑥 ≈ (card‘𝐴)) |
| 24 | 23 | a1i 11 |
. . . . 5
⊢ ((ω
⊆ (card‘𝐴)
∧ 𝑥 ∈ On) →
((card‘𝐴) = suc 𝑥 → ¬ 𝑥 ≈ (card‘𝐴))) |
| 25 | 15, 24 | pm2.65d 196 |
. . . 4
⊢ ((ω
⊆ (card‘𝐴)
∧ 𝑥 ∈ On) →
¬ (card‘𝐴) = suc
𝑥) |
| 26 | 25 | nrexdv 3149 |
. . 3
⊢ (ω
⊆ (card‘𝐴)
→ ¬ ∃𝑥
∈ On (card‘𝐴) =
suc 𝑥) |
| 27 | | peano1 7910 |
. . . . . 6
⊢ ∅
∈ ω |
| 28 | | ssel 3977 |
. . . . . 6
⊢ (ω
⊆ (card‘𝐴)
→ (∅ ∈ ω → ∅ ∈ (card‘𝐴))) |
| 29 | 27, 28 | mpi 20 |
. . . . 5
⊢ (ω
⊆ (card‘𝐴)
→ ∅ ∈ (card‘𝐴)) |
| 30 | | n0i 4340 |
. . . . 5
⊢ (∅
∈ (card‘𝐴)
→ ¬ (card‘𝐴)
= ∅) |
| 31 | | cardon 9984 |
. . . . . . . . 9
⊢
(card‘𝐴)
∈ On |
| 32 | 31 | onordi 6495 |
. . . . . . . 8
⊢ Ord
(card‘𝐴) |
| 33 | | ordzsl 7866 |
. . . . . . . 8
⊢ (Ord
(card‘𝐴) ↔
((card‘𝐴) = ∅
∨ ∃𝑥 ∈ On
(card‘𝐴) = suc 𝑥 ∨ Lim (card‘𝐴))) |
| 34 | 32, 33 | mpbi 230 |
. . . . . . 7
⊢
((card‘𝐴) =
∅ ∨ ∃𝑥
∈ On (card‘𝐴) =
suc 𝑥 ∨ Lim
(card‘𝐴)) |
| 35 | | 3orass 1090 |
. . . . . . 7
⊢
(((card‘𝐴) =
∅ ∨ ∃𝑥
∈ On (card‘𝐴) =
suc 𝑥 ∨ Lim
(card‘𝐴)) ↔
((card‘𝐴) = ∅
∨ (∃𝑥 ∈ On
(card‘𝐴) = suc 𝑥 ∨ Lim (card‘𝐴)))) |
| 36 | 34, 35 | mpbi 230 |
. . . . . 6
⊢
((card‘𝐴) =
∅ ∨ (∃𝑥
∈ On (card‘𝐴) =
suc 𝑥 ∨ Lim
(card‘𝐴))) |
| 37 | 36 | ori 862 |
. . . . 5
⊢ (¬
(card‘𝐴) = ∅
→ (∃𝑥 ∈ On
(card‘𝐴) = suc 𝑥 ∨ Lim (card‘𝐴))) |
| 38 | 29, 30, 37 | 3syl 18 |
. . . 4
⊢ (ω
⊆ (card‘𝐴)
→ (∃𝑥 ∈ On
(card‘𝐴) = suc 𝑥 ∨ Lim (card‘𝐴))) |
| 39 | 38 | ord 865 |
. . 3
⊢ (ω
⊆ (card‘𝐴)
→ (¬ ∃𝑥
∈ On (card‘𝐴) =
suc 𝑥 → Lim
(card‘𝐴))) |
| 40 | 26, 39 | mpd 15 |
. 2
⊢ (ω
⊆ (card‘𝐴)
→ Lim (card‘𝐴)) |
| 41 | | limomss 7892 |
. 2
⊢ (Lim
(card‘𝐴) →
ω ⊆ (card‘𝐴)) |
| 42 | 40, 41 | impbii 209 |
1
⊢ (ω
⊆ (card‘𝐴)
↔ Lim (card‘𝐴)) |