Metamath Proof Explorer

Theorem alephgch

Description: If ( alephsuc A ) is equinumerous to the powerset of ( alephA ) , then ( alephA ) is a GCH-set. (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion alephgch ⊢ℵ⁡suc⁡A≈𝒫ℵ⁡A→ℵ⁡A∈GCH

Proof

Step Hyp Ref Expression
1 alephnbtwn2 ⊢¬ℵ⁡A≺x∧x≺ℵ⁡suc⁡A
2 sdomen2 ⊢ℵ⁡suc⁡A≈𝒫ℵ⁡A→x≺ℵ⁡suc⁡A↔x≺𝒫ℵ⁡A
3 2 anbi2d ⊢ℵ⁡suc⁡A≈𝒫ℵ⁡A→ℵ⁡A≺x∧x≺ℵ⁡suc⁡A↔ℵ⁡A≺x∧x≺𝒫ℵ⁡A
4 1 3 mtbii ⊢ℵ⁡suc⁡A≈𝒫ℵ⁡A→¬ℵ⁡A≺x∧x≺𝒫ℵ⁡A
5 4 alrimiv ⊢ℵ⁡suc⁡A≈𝒫ℵ⁡A→∀x¬ℵ⁡A≺x∧x≺𝒫ℵ⁡A
6 5 olcd ⊢ℵ⁡suc⁡A≈𝒫ℵ⁡A→ℵ⁡A∈Fin∨∀x¬ℵ⁡A≺x∧x≺𝒫ℵ⁡A
7 fvex ⊢ℵ⁡A∈V
8 elgch ⊢ℵ⁡A∈V→ℵ⁡A∈GCH↔ℵ⁡A∈Fin∨∀x¬ℵ⁡A≺x∧x≺𝒫ℵ⁡A
9 7 8 ax-mp ⊢ℵ⁡A∈GCH↔ℵ⁡A∈Fin∨∀x¬ℵ⁡A≺x∧x≺𝒫ℵ⁡A
10 6 9 sylibr ⊢ℵ⁡suc⁡A≈𝒫ℵ⁡A→ℵ⁡A∈GCH