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 \left(1_{𝑜}\right)\preccurlyeq \left({2_{𝑜}}^{\aleph \left(\varnothing \right)}\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-1o	$$⊢1_{𝑜}=\mathrm{suc}\varnothing$$
2	1	fveq2i	$$⊢\aleph \left(1_{𝑜}\right)=\aleph \left(\mathrm{suc}\varnothing \right)$$
3		alephsucpw	$$⊢\aleph \left(\mathrm{suc}\varnothing \right)\preccurlyeq 𝒫\aleph \left(\varnothing \right)$$
4		fvex	$$⊢\aleph \left(\varnothing \right)\in \mathrm{V}$$
5	4	pw2en	$$⊢𝒫\aleph \left(\varnothing \right)\approx \left({2_{𝑜}}^{\aleph \left(\varnothing \right)}\right)$$
6		domen2	$$⊢𝒫\aleph \left(\varnothing \right)\approx \left({2_{𝑜}}^{\aleph \left(\varnothing \right)}\right)\to \left(\aleph \left(\mathrm{suc}\varnothing \right)\preccurlyeq 𝒫\aleph \left(\varnothing \right)\leftrightarrow \aleph \left(\mathrm{suc}\varnothing \right)\preccurlyeq \left({2_{𝑜}}^{\aleph \left(\varnothing \right)}\right)\right)$$
7	5 6	ax-mp	$$⊢\aleph \left(\mathrm{suc}\varnothing \right)\preccurlyeq 𝒫\aleph \left(\varnothing \right)\leftrightarrow \aleph \left(\mathrm{suc}\varnothing \right)\preccurlyeq \left({2_{𝑜}}^{\aleph \left(\varnothing \right)}\right)$$
8	3 7	mpbi	$$⊢\aleph \left(\mathrm{suc}\varnothing \right)\preccurlyeq \left({2_{𝑜}}^{\aleph \left(\varnothing \right)}\right)$$
9	2 8	eqbrtri	$$⊢\aleph \left(1_{𝑜}\right)\preccurlyeq \left({2_{𝑜}}^{\aleph \left(\varnothing \right)}\right)$$