Theorem alephsucpw2

Description: The power set of an aleph is not strictly dominated by the successor aleph. (The Generalized Continuum Hypothesis says they are equinumerous, see gch3 or gchaleph2 .) The transposed form alephsucpw cannot be proven without the AC, and is in fact equivalent to it. (Contributed by Mario Carneiro, 2-Feb-2013)

	Ref	Expression
Assertion	alephsucpw2	|- -. ~P ( aleph ` A ) ~< ( aleph ` suc A )

Proof

Step	Hyp	Ref	Expression
1		fvex	|- ( aleph ` A ) e. _V
2	1	canth2	|- ( aleph ` A ) ~< ~P ( aleph ` A )
3		alephnbtwn2	|- -. ( ( aleph ` A ) ~< ~P ( aleph ` A ) /\ ~P ( aleph ` A ) ~< ( aleph ` suc A ) )
4	2 3	mptnan	|- -. ~P ( aleph ` A ) ~< ( aleph ` suc A )