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	⊢ ( ℵ ‘ 1o ) ≼ ( 2o ↑m ( ℵ ‘ ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		df-1o	⊢ 1o = suc ∅
2	1	fveq2i	⊢ ( ℵ ‘ 1o ) = ( ℵ ‘ suc ∅ )
3		alephsucpw	⊢ ( ℵ ‘ suc ∅ ) ≼ 𝒫 ( ℵ ‘ ∅ )
4		fvex	⊢ ( ℵ ‘ ∅ ) ∈ V
5	4	pw2en	⊢ 𝒫 ( ℵ ‘ ∅ ) ≈ ( 2o ↑m ( ℵ ‘ ∅ ) )
6		domen2	⊢ ( 𝒫 ( ℵ ‘ ∅ ) ≈ ( 2o ↑m ( ℵ ‘ ∅ ) ) → ( ( ℵ ‘ suc ∅ ) ≼ 𝒫 ( ℵ ‘ ∅ ) ↔ ( ℵ ‘ suc ∅ ) ≼ ( 2o ↑m ( ℵ ‘ ∅ ) ) ) )
7	5 6	ax-mp	⊢ ( ( ℵ ‘ suc ∅ ) ≼ 𝒫 ( ℵ ‘ ∅ ) ↔ ( ℵ ‘ suc ∅ ) ≼ ( 2o ↑m ( ℵ ‘ ∅ ) ) )
8	3 7	mpbi	⊢ ( ℵ ‘ suc ∅ ) ≼ ( 2o ↑m ( ℵ ‘ ∅ ) )
9	2 8	eqbrtri	⊢ ( ℵ ‘ 1o ) ≼ ( 2o ↑m ( ℵ ‘ ∅ ) )