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