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 ( ( 𝐴 ∈ On ∧ ( ℵ ‘ 𝐴 ) ∈ GCH ∧ ( ℵ ‘ suc 𝐴 ) ∈ GCH ) → ( ℵ ‘ suc 𝐴 ) ≈ 𝒫 ( ℵ ‘ 𝐴 ) )

Proof

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