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 ` (/) ) )