Metamath Proof Explorer

Theorem aleph1

Description: The set exponentiation of 2 to the aleph-zero has cardinality of at least aleph-one. (If we were to assume the Continuum Hypothesis, their cardinalities would be the same.) (Contributed by NM, 7-Jul-2004)

Ref Expression
Assertion aleph1 
|- ( aleph ` 1o ) ~<_ ( 2o ^m ( aleph ` (/) ) )

Proof

Step Hyp Ref Expression
1 df-1o 
 |-  1o = suc (/)
2 1 fveq2i 
 |-  ( aleph ` 1o ) = ( aleph ` suc (/) )
3 alephsucpw 
 |-  ( aleph ` suc (/) ) ~<_ ~P ( aleph ` (/) )
4 fvex 
 |-  ( aleph ` (/) ) e. _V
5 4 pw2en 
 |-  ~P ( aleph ` (/) ) ~~ ( 2o ^m ( aleph ` (/) ) )
6 domen2 
 |-  ( ~P ( aleph ` (/) ) ~~ ( 2o ^m ( aleph ` (/) ) ) -> ( ( aleph ` suc (/) ) ~<_ ~P ( aleph ` (/) ) <-> ( aleph ` suc (/) ) ~<_ ( 2o ^m ( aleph ` (/) ) ) ) )
7 5 6 ax-mp 
 |-  ( ( aleph ` suc (/) ) ~<_ ~P ( aleph ` (/) ) <-> ( aleph ` suc (/) ) ~<_ ( 2o ^m ( aleph ` (/) ) ) )
8 3 7 mpbi 
 |-  ( aleph ` suc (/) ) ~<_ ( 2o ^m ( aleph ` (/) ) )
9 2 8 eqbrtri 
 |-  ( aleph ` 1o ) ~<_ ( 2o ^m ( aleph ` (/) ) )