Proof of Theorem gchaleph
| Step | Hyp | Ref
| Expression |
| 1 | | alephsucpw2 10151 |
. . 3
⊢ ¬
𝒫 (ℵ‘𝐴)
≺ (ℵ‘suc 𝐴) |
| 2 | | alephon 10109 |
. . . . 5
⊢
(ℵ‘suc 𝐴) ∈ On |
| 3 | | onenon 9989 |
. . . . 5
⊢
((ℵ‘suc 𝐴) ∈ On → (ℵ‘suc 𝐴) ∈ dom
card) |
| 4 | 2, 3 | ax-mp 5 |
. . . 4
⊢
(ℵ‘suc 𝐴) ∈ dom card |
| 5 | | simp3 1139 |
. . . 4
⊢ ((𝐴 ∈ On ∧
(ℵ‘𝐴) ∈
GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) → 𝒫
(ℵ‘𝐴) ∈
dom card) |
| 6 | | domtri2 10029 |
. . . 4
⊢
(((ℵ‘suc 𝐴) ∈ dom card ∧ 𝒫
(ℵ‘𝐴) ∈
dom card) → ((ℵ‘suc 𝐴) ≼ 𝒫 (ℵ‘𝐴) ↔ ¬ 𝒫
(ℵ‘𝐴) ≺
(ℵ‘suc 𝐴))) |
| 7 | 4, 5, 6 | sylancr 587 |
. . 3
⊢ ((𝐴 ∈ On ∧
(ℵ‘𝐴) ∈
GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) →
((ℵ‘suc 𝐴)
≼ 𝒫 (ℵ‘𝐴) ↔ ¬ 𝒫
(ℵ‘𝐴) ≺
(ℵ‘suc 𝐴))) |
| 8 | 1, 7 | mpbiri 258 |
. 2
⊢ ((𝐴 ∈ On ∧
(ℵ‘𝐴) ∈
GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) → (ℵ‘suc
𝐴) ≼ 𝒫
(ℵ‘𝐴)) |
| 9 | | fvex 6919 |
. . . . . . 7
⊢
(ℵ‘𝐴)
∈ V |
| 10 | | simp1 1137 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧
(ℵ‘𝐴) ∈
GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) → 𝐴 ∈ On) |
| 11 | | alephgeom 10122 |
. . . . . . . 8
⊢ (𝐴 ∈ On ↔ ω
⊆ (ℵ‘𝐴)) |
| 12 | 10, 11 | sylib 218 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧
(ℵ‘𝐴) ∈
GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) → ω ⊆
(ℵ‘𝐴)) |
| 13 | | ssdomg 9040 |
. . . . . . 7
⊢
((ℵ‘𝐴)
∈ V → (ω ⊆ (ℵ‘𝐴) → ω ≼
(ℵ‘𝐴))) |
| 14 | 9, 12, 13 | mpsyl 68 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧
(ℵ‘𝐴) ∈
GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) → ω ≼
(ℵ‘𝐴)) |
| 15 | | domnsym 9139 |
. . . . . 6
⊢ (ω
≼ (ℵ‘𝐴)
→ ¬ (ℵ‘𝐴) ≺ ω) |
| 16 | 14, 15 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ On ∧
(ℵ‘𝐴) ∈
GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) → ¬
(ℵ‘𝐴) ≺
ω) |
| 17 | | isfinite 9692 |
. . . . 5
⊢
((ℵ‘𝐴)
∈ Fin ↔ (ℵ‘𝐴) ≺ ω) |
| 18 | 16, 17 | sylnibr 329 |
. . . 4
⊢ ((𝐴 ∈ On ∧
(ℵ‘𝐴) ∈
GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) → ¬
(ℵ‘𝐴) ∈
Fin) |
| 19 | | simp2 1138 |
. . . . 5
⊢ ((𝐴 ∈ On ∧
(ℵ‘𝐴) ∈
GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) →
(ℵ‘𝐴) ∈
GCH) |
| 20 | | alephordilem1 10113 |
. . . . . 6
⊢ (𝐴 ∈ On →
(ℵ‘𝐴) ≺
(ℵ‘suc 𝐴)) |
| 21 | 20 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝐴 ∈ On ∧
(ℵ‘𝐴) ∈
GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) →
(ℵ‘𝐴) ≺
(ℵ‘suc 𝐴)) |
| 22 | | gchi 10664 |
. . . . . 6
⊢
(((ℵ‘𝐴)
∈ GCH ∧ (ℵ‘𝐴) ≺ (ℵ‘suc 𝐴) ∧ (ℵ‘suc 𝐴) ≺ 𝒫
(ℵ‘𝐴)) →
(ℵ‘𝐴) ∈
Fin) |
| 23 | 22 | 3expia 1122 |
. . . . 5
⊢
(((ℵ‘𝐴)
∈ GCH ∧ (ℵ‘𝐴) ≺ (ℵ‘suc 𝐴)) → ((ℵ‘suc
𝐴) ≺ 𝒫
(ℵ‘𝐴) →
(ℵ‘𝐴) ∈
Fin)) |
| 24 | 19, 21, 23 | syl2anc 584 |
. . . 4
⊢ ((𝐴 ∈ On ∧
(ℵ‘𝐴) ∈
GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) →
((ℵ‘suc 𝐴)
≺ 𝒫 (ℵ‘𝐴) → (ℵ‘𝐴) ∈ Fin)) |
| 25 | 18, 24 | mtod 198 |
. . 3
⊢ ((𝐴 ∈ On ∧
(ℵ‘𝐴) ∈
GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) → ¬
(ℵ‘suc 𝐴)
≺ 𝒫 (ℵ‘𝐴)) |
| 26 | | domtri2 10029 |
. . . 4
⊢
((𝒫 (ℵ‘𝐴) ∈ dom card ∧ (ℵ‘suc
𝐴) ∈ dom card) →
(𝒫 (ℵ‘𝐴) ≼ (ℵ‘suc 𝐴) ↔ ¬
(ℵ‘suc 𝐴)
≺ 𝒫 (ℵ‘𝐴))) |
| 27 | 5, 4, 26 | sylancl 586 |
. . 3
⊢ ((𝐴 ∈ On ∧
(ℵ‘𝐴) ∈
GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) → (𝒫
(ℵ‘𝐴) ≼
(ℵ‘suc 𝐴)
↔ ¬ (ℵ‘suc 𝐴) ≺ 𝒫 (ℵ‘𝐴))) |
| 28 | 25, 27 | mpbird 257 |
. 2
⊢ ((𝐴 ∈ On ∧
(ℵ‘𝐴) ∈
GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) → 𝒫
(ℵ‘𝐴) ≼
(ℵ‘suc 𝐴)) |
| 29 | | sbth 9133 |
. 2
⊢
(((ℵ‘suc 𝐴) ≼ 𝒫 (ℵ‘𝐴) ∧ 𝒫
(ℵ‘𝐴) ≼
(ℵ‘suc 𝐴))
→ (ℵ‘suc 𝐴) ≈ 𝒫 (ℵ‘𝐴)) |
| 30 | 8, 28, 29 | syl2anc 584 |
1
⊢ ((𝐴 ∈ On ∧
(ℵ‘𝐴) ∈
GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) → (ℵ‘suc
𝐴) ≈ 𝒫
(ℵ‘𝐴)) |