This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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