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

Metamath Proof Explorer

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 )