Theorem alephsucpw

Description: The power set of an aleph dominates the successor aleph. (The Generalized Continuum Hypothesis says they are equinumerous, see gch3 or gchaleph2 .) (Contributed by NM, 27-Aug-2005)

	Ref	Expression
Assertion	alephsucpw	⊢ ( ℵ ‘ suc 𝐴 ) ≼ 𝒫 ( ℵ ‘ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		alephsucpw2	⊢ ¬ 𝒫 ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ suc 𝐴 )
2		fvex	⊢ ( ℵ ‘ suc 𝐴 ) ∈ V
3		fvex	⊢ ( ℵ ‘ 𝐴 ) ∈ V
4	3	pwex	⊢ 𝒫 ( ℵ ‘ 𝐴 ) ∈ V
5		domtri	⊢ ( ( ( ℵ ‘ suc 𝐴 ) ∈ V ∧ 𝒫 ( ℵ ‘ 𝐴 ) ∈ V ) → ( ( ℵ ‘ suc 𝐴 ) ≼ 𝒫 ( ℵ ‘ 𝐴 ) ↔ ¬ 𝒫 ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ suc 𝐴 ) ) )
6	2 4 5	mp2an	⊢ ( ( ℵ ‘ suc 𝐴 ) ≼ 𝒫 ( ℵ ‘ 𝐴 ) ↔ ¬ 𝒫 ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ suc 𝐴 ) )
7	1 6	mpbir	⊢ ( ℵ ‘ suc 𝐴 ) ≼ 𝒫 ( ℵ ‘ 𝐴 )