Proof of Theorem gchaleph
Step | Hyp | Ref
| Expression |
1 | | alephsucpw2 9851 |
. . 3
⊢ ¬
𝒫 (ℵ‘𝐴)
≺ (ℵ‘suc 𝐴) |
2 | | alephon 9809 |
. . . . 5
⊢
(ℵ‘suc 𝐴) ∈ On |
3 | | onenon 9691 |
. . . . 5
⊢
((ℵ‘suc 𝐴) ∈ On → (ℵ‘suc 𝐴) ∈ dom
card) |
4 | 2, 3 | ax-mp 5 |
. . . 4
⊢
(ℵ‘suc 𝐴) ∈ dom card |
5 | | simp3 1136 |
. . . 4
⊢ ((𝐴 ∈ On ∧
(ℵ‘𝐴) ∈
GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) → 𝒫
(ℵ‘𝐴) ∈
dom card) |
6 | | domtri2 9731 |
. . . 4
⊢
(((ℵ‘suc 𝐴) ∈ dom card ∧ 𝒫
(ℵ‘𝐴) ∈
dom card) → ((ℵ‘suc 𝐴) ≼ 𝒫 (ℵ‘𝐴) ↔ ¬ 𝒫
(ℵ‘𝐴) ≺
(ℵ‘suc 𝐴))) |
7 | 4, 5, 6 | sylancr 586 |
. . 3
⊢ ((𝐴 ∈ On ∧
(ℵ‘𝐴) ∈
GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) →
((ℵ‘suc 𝐴)
≼ 𝒫 (ℵ‘𝐴) ↔ ¬ 𝒫
(ℵ‘𝐴) ≺
(ℵ‘suc 𝐴))) |
8 | 1, 7 | mpbiri 257 |
. 2
⊢ ((𝐴 ∈ On ∧
(ℵ‘𝐴) ∈
GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) → (ℵ‘suc
𝐴) ≼ 𝒫
(ℵ‘𝐴)) |
9 | | fvex 6781 |
. . . . . . 7
⊢
(ℵ‘𝐴)
∈ V |
10 | | simp1 1134 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧
(ℵ‘𝐴) ∈
GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) → 𝐴 ∈ On) |
11 | | alephgeom 9822 |
. . . . . . . 8
⊢ (𝐴 ∈ On ↔ ω
⊆ (ℵ‘𝐴)) |
12 | 10, 11 | sylib 217 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧
(ℵ‘𝐴) ∈
GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) → ω ⊆
(ℵ‘𝐴)) |
13 | | ssdomg 8757 |
. . . . . . 7
⊢
((ℵ‘𝐴)
∈ V → (ω ⊆ (ℵ‘𝐴) → ω ≼
(ℵ‘𝐴))) |
14 | 9, 12, 13 | mpsyl 68 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧
(ℵ‘𝐴) ∈
GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) → ω ≼
(ℵ‘𝐴)) |
15 | | domnsym 8855 |
. . . . . 6
⊢ (ω
≼ (ℵ‘𝐴)
→ ¬ (ℵ‘𝐴) ≺ ω) |
16 | 14, 15 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ On ∧
(ℵ‘𝐴) ∈
GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) → ¬
(ℵ‘𝐴) ≺
ω) |
17 | | isfinite 9371 |
. . . . 5
⊢
((ℵ‘𝐴)
∈ Fin ↔ (ℵ‘𝐴) ≺ ω) |
18 | 16, 17 | sylnibr 328 |
. . . 4
⊢ ((𝐴 ∈ On ∧
(ℵ‘𝐴) ∈
GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) → ¬
(ℵ‘𝐴) ∈
Fin) |
19 | | simp2 1135 |
. . . . 5
⊢ ((𝐴 ∈ On ∧
(ℵ‘𝐴) ∈
GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) →
(ℵ‘𝐴) ∈
GCH) |
20 | | alephordilem1 9813 |
. . . . . 6
⊢ (𝐴 ∈ On →
(ℵ‘𝐴) ≺
(ℵ‘suc 𝐴)) |
21 | 20 | 3ad2ant1 1131 |
. . . . 5
⊢ ((𝐴 ∈ On ∧
(ℵ‘𝐴) ∈
GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) →
(ℵ‘𝐴) ≺
(ℵ‘suc 𝐴)) |
22 | | gchi 10364 |
. . . . . 6
⊢
(((ℵ‘𝐴)
∈ GCH ∧ (ℵ‘𝐴) ≺ (ℵ‘suc 𝐴) ∧ (ℵ‘suc 𝐴) ≺ 𝒫
(ℵ‘𝐴)) →
(ℵ‘𝐴) ∈
Fin) |
23 | 22 | 3expia 1119 |
. . . . 5
⊢
(((ℵ‘𝐴)
∈ GCH ∧ (ℵ‘𝐴) ≺ (ℵ‘suc 𝐴)) → ((ℵ‘suc
𝐴) ≺ 𝒫
(ℵ‘𝐴) →
(ℵ‘𝐴) ∈
Fin)) |
24 | 19, 21, 23 | syl2anc 583 |
. . . 4
⊢ ((𝐴 ∈ On ∧
(ℵ‘𝐴) ∈
GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) →
((ℵ‘suc 𝐴)
≺ 𝒫 (ℵ‘𝐴) → (ℵ‘𝐴) ∈ Fin)) |
25 | 18, 24 | mtod 197 |
. . 3
⊢ ((𝐴 ∈ On ∧
(ℵ‘𝐴) ∈
GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) → ¬
(ℵ‘suc 𝐴)
≺ 𝒫 (ℵ‘𝐴)) |
26 | | domtri2 9731 |
. . . 4
⊢
((𝒫 (ℵ‘𝐴) ∈ dom card ∧ (ℵ‘suc
𝐴) ∈ dom card) →
(𝒫 (ℵ‘𝐴) ≼ (ℵ‘suc 𝐴) ↔ ¬
(ℵ‘suc 𝐴)
≺ 𝒫 (ℵ‘𝐴))) |
27 | 5, 4, 26 | sylancl 585 |
. . 3
⊢ ((𝐴 ∈ On ∧
(ℵ‘𝐴) ∈
GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) → (𝒫
(ℵ‘𝐴) ≼
(ℵ‘suc 𝐴)
↔ ¬ (ℵ‘suc 𝐴) ≺ 𝒫 (ℵ‘𝐴))) |
28 | 25, 27 | mpbird 256 |
. 2
⊢ ((𝐴 ∈ On ∧
(ℵ‘𝐴) ∈
GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) → 𝒫
(ℵ‘𝐴) ≼
(ℵ‘suc 𝐴)) |
29 | | sbth 8849 |
. 2
⊢
(((ℵ‘suc 𝐴) ≼ 𝒫 (ℵ‘𝐴) ∧ 𝒫
(ℵ‘𝐴) ≼
(ℵ‘suc 𝐴))
→ (ℵ‘suc 𝐴) ≈ 𝒫 (ℵ‘𝐴)) |
30 | 8, 28, 29 | syl2anc 583 |
1
⊢ ((𝐴 ∈ On ∧
(ℵ‘𝐴) ∈
GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) → (ℵ‘suc
𝐴) ≈ 𝒫
(ℵ‘𝐴)) |