Step |
Hyp |
Ref |
Expression |
1 |
|
simpr |
⊢ ( ( GCH = V ∧ 𝑥 ∈ On ) → 𝑥 ∈ On ) |
2 |
|
fvex |
⊢ ( ℵ ‘ 𝑥 ) ∈ V |
3 |
|
simpl |
⊢ ( ( GCH = V ∧ 𝑥 ∈ On ) → GCH = V ) |
4 |
2 3
|
eleqtrrid |
⊢ ( ( GCH = V ∧ 𝑥 ∈ On ) → ( ℵ ‘ 𝑥 ) ∈ GCH ) |
5 |
|
fvex |
⊢ ( ℵ ‘ suc 𝑥 ) ∈ V |
6 |
5 3
|
eleqtrrid |
⊢ ( ( GCH = V ∧ 𝑥 ∈ On ) → ( ℵ ‘ suc 𝑥 ) ∈ GCH ) |
7 |
|
gchaleph2 |
⊢ ( ( 𝑥 ∈ On ∧ ( ℵ ‘ 𝑥 ) ∈ GCH ∧ ( ℵ ‘ suc 𝑥 ) ∈ GCH ) → ( ℵ ‘ suc 𝑥 ) ≈ 𝒫 ( ℵ ‘ 𝑥 ) ) |
8 |
1 4 6 7
|
syl3anc |
⊢ ( ( GCH = V ∧ 𝑥 ∈ On ) → ( ℵ ‘ suc 𝑥 ) ≈ 𝒫 ( ℵ ‘ 𝑥 ) ) |
9 |
8
|
ralrimiva |
⊢ ( GCH = V → ∀ 𝑥 ∈ On ( ℵ ‘ suc 𝑥 ) ≈ 𝒫 ( ℵ ‘ 𝑥 ) ) |
10 |
|
alephgch |
⊢ ( ( ℵ ‘ suc 𝑥 ) ≈ 𝒫 ( ℵ ‘ 𝑥 ) → ( ℵ ‘ 𝑥 ) ∈ GCH ) |
11 |
10
|
ralimi |
⊢ ( ∀ 𝑥 ∈ On ( ℵ ‘ suc 𝑥 ) ≈ 𝒫 ( ℵ ‘ 𝑥 ) → ∀ 𝑥 ∈ On ( ℵ ‘ 𝑥 ) ∈ GCH ) |
12 |
|
alephfnon |
⊢ ℵ Fn On |
13 |
|
ffnfv |
⊢ ( ℵ : On ⟶ GCH ↔ ( ℵ Fn On ∧ ∀ 𝑥 ∈ On ( ℵ ‘ 𝑥 ) ∈ GCH ) ) |
14 |
12 13
|
mpbiran |
⊢ ( ℵ : On ⟶ GCH ↔ ∀ 𝑥 ∈ On ( ℵ ‘ 𝑥 ) ∈ GCH ) |
15 |
11 14
|
sylibr |
⊢ ( ∀ 𝑥 ∈ On ( ℵ ‘ suc 𝑥 ) ≈ 𝒫 ( ℵ ‘ 𝑥 ) → ℵ : On ⟶ GCH ) |
16 |
15
|
frnd |
⊢ ( ∀ 𝑥 ∈ On ( ℵ ‘ suc 𝑥 ) ≈ 𝒫 ( ℵ ‘ 𝑥 ) → ran ℵ ⊆ GCH ) |
17 |
|
gch2 |
⊢ ( GCH = V ↔ ran ℵ ⊆ GCH ) |
18 |
16 17
|
sylibr |
⊢ ( ∀ 𝑥 ∈ On ( ℵ ‘ suc 𝑥 ) ≈ 𝒫 ( ℵ ‘ 𝑥 ) → GCH = V ) |
19 |
9 18
|
impbii |
⊢ ( GCH = V ↔ ∀ 𝑥 ∈ On ( ℵ ‘ suc 𝑥 ) ≈ 𝒫 ( ℵ ‘ 𝑥 ) ) |