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 )