Metamath Proof Explorer

Theorem gchaleph2

Description: If ( alephA ) and ( alephsuc A ) are GCH-sets, then the successor aleph ( alephsuc A ) is equinumerous to the powerset of ( alephA ) . (Contributed by Mario Carneiro, 31-May-2015)

Ref Expression
Assertion gchaleph2 ⊢ A ∈ On ∧ ℵ ⁡ A ∈ GCH ∧ ℵ ⁡ suc ⁡ A ∈ GCH → ℵ ⁡ suc ⁡ A ≈ 𝒫 ℵ ⁡ A

Proof

Step Hyp Ref Expression
1 harcl ⊢ har ⁡ ℵ ⁡ A ∈ On
2 alephon ⊢ ℵ ⁡ A ∈ On
3 onenon ⊢ ℵ ⁡ A ∈ On → ℵ ⁡ A ∈ dom ⁡ card
4 harsdom ⊢ ℵ ⁡ A ∈ dom ⁡ card → ℵ ⁡ A ≺ har ⁡ ℵ ⁡ A
5 2 3 4 mp2b ⊢ ℵ ⁡ A ≺ har ⁡ ℵ ⁡ A
6 simp1 ⊢ A ∈ On ∧ ℵ ⁡ A ∈ GCH ∧ ℵ ⁡ suc ⁡ A ∈ GCH → A ∈ On
7 alephgeom ⊢ A ∈ On ↔ ω ⊆ ℵ ⁡ A
8 6 7 sylib ⊢ A ∈ On ∧ ℵ ⁡ A ∈ GCH ∧ ℵ ⁡ suc ⁡ A ∈ GCH → ω ⊆ ℵ ⁡ A
9 ssdomg ⊢ ℵ ⁡ A ∈ On → ω ⊆ ℵ ⁡ A → ω ≼ ℵ ⁡ A
10 2 8 9 mpsyl ⊢ A ∈ On ∧ ℵ ⁡ A ∈ GCH ∧ ℵ ⁡ suc ⁡ A ∈ GCH → ω ≼ ℵ ⁡ A
11 simp2 ⊢ A ∈ On ∧ ℵ ⁡ A ∈ GCH ∧ ℵ ⁡ suc ⁡ A ∈ GCH → ℵ ⁡ A ∈ GCH
12 alephsuc ⊢ A ∈ On → ℵ ⁡ suc ⁡ A = har ⁡ ℵ ⁡ A
13 6 12 syl ⊢ A ∈ On ∧ ℵ ⁡ A ∈ GCH ∧ ℵ ⁡ suc ⁡ A ∈ GCH → ℵ ⁡ suc ⁡ A = har ⁡ ℵ ⁡ A
14 simp3 ⊢ A ∈ On ∧ ℵ ⁡ A ∈ GCH ∧ ℵ ⁡ suc ⁡ A ∈ GCH → ℵ ⁡ suc ⁡ A ∈ GCH
15 13 14 eqeltrrd ⊢ A ∈ On ∧ ℵ ⁡ A ∈ GCH ∧ ℵ ⁡ suc ⁡ A ∈ GCH → har ⁡ ℵ ⁡ A ∈ GCH
16 gchpwdom ⊢ ω ≼ ℵ ⁡ A ∧ ℵ ⁡ A ∈ GCH ∧ har ⁡ ℵ ⁡ A ∈ GCH → ℵ ⁡ A ≺ har ⁡ ℵ ⁡ A ↔ 𝒫 ℵ ⁡ A ≼ har ⁡ ℵ ⁡ A
17 10 11 15 16 syl3anc ⊢ A ∈ On ∧ ℵ ⁡ A ∈ GCH ∧ ℵ ⁡ suc ⁡ A ∈ GCH → ℵ ⁡ A ≺ har ⁡ ℵ ⁡ A ↔ 𝒫 ℵ ⁡ A ≼ har ⁡ ℵ ⁡ A
18 5 17 mpbii ⊢ A ∈ On ∧ ℵ ⁡ A ∈ GCH ∧ ℵ ⁡ suc ⁡ A ∈ GCH → 𝒫 ℵ ⁡ A ≼ har ⁡ ℵ ⁡ A
19 ondomen ⊢ har ⁡ ℵ ⁡ A ∈ On ∧ 𝒫 ℵ ⁡ A ≼ har ⁡ ℵ ⁡ A → 𝒫 ℵ ⁡ A ∈ dom ⁡ card
20 1 18 19 sylancr ⊢ A ∈ On ∧ ℵ ⁡ A ∈ GCH ∧ ℵ ⁡ suc ⁡ A ∈ GCH → 𝒫 ℵ ⁡ A ∈ dom ⁡ card
21 gchaleph ⊢ A ∈ On ∧ ℵ ⁡ A ∈ GCH ∧ 𝒫 ℵ ⁡ A ∈ dom ⁡ card → ℵ ⁡ suc ⁡ A ≈ 𝒫 ℵ ⁡ A
22 20 21 syld3an3 ⊢ A ∈ On ∧ ℵ ⁡ A ∈ GCH ∧ ℵ ⁡ suc ⁡ A ∈ GCH → ℵ ⁡ suc ⁡ A ≈ 𝒫 ℵ ⁡ A