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	|- ( aleph ` suc A ) ~<_ ~P ( aleph ` A )

Proof

Step	Hyp	Ref	Expression
1		alephsucpw2	|- -. ~P ( aleph ` A ) ~< ( aleph ` suc A )
2		fvex	|- ( aleph ` suc A ) e. _V
3		fvex	|- ( aleph ` A ) e. _V
4	3	pwex	|- ~P ( aleph ` A ) e. _V
5		domtri	|- ( ( ( aleph ` suc A ) e. _V /\ ~P ( aleph ` A ) e. _V ) -> ( ( aleph ` suc A ) ~<_ ~P ( aleph ` A ) <-> -. ~P ( aleph ` A ) ~< ( aleph ` suc A ) ) )
6	2 4 5	mp2an	|- ( ( aleph ` suc A ) ~<_ ~P ( aleph ` A ) <-> -. ~P ( aleph ` A ) ~< ( aleph ` suc A ) )
7	1 6	mpbir	|- ( aleph ` suc A ) ~<_ ~P ( aleph ` A )