Theorem aleph1re

Description: There are at least aleph-one real numbers. (Contributed by NM, 2-Feb-2005)

	Ref	Expression
Assertion	aleph1re	$$⊢\aleph \left(1_{𝑜}\right)\preccurlyeq ℝ$$

Proof

Step	Hyp	Ref	Expression
1		aleph0	$$⊢\aleph \left(\varnothing \right)=\mathrm{\omega }$$
2		nnenom	$$⊢\mathbb{N}\approx \mathrm{\omega }$$
3	2	ensymi	$$⊢\mathrm{\omega }\approx \mathbb{N}$$
4	1 3	eqbrtri	$$⊢\aleph \left(\varnothing \right)\approx \mathbb{N}$$
5		ruc	$$⊢\mathbb{N}\prec ℝ$$
6		ensdomtr	$$⊢\left(\aleph \left(\varnothing \right)\approx \mathbb{N}\wedge \mathbb{N}\prec ℝ\right)\to \aleph \left(\varnothing \right)\prec ℝ$$
7	4 5 6	mp2an	$$⊢\aleph \left(\varnothing \right)\prec ℝ$$
8		alephnbtwn2	$$⊢\neg \left(\aleph \left(\varnothing \right)\prec ℝ\wedge ℝ\prec \aleph \left(\mathrm{suc}\varnothing \right)\right)$$
9	7 8	mptnan	$$⊢\neg ℝ\prec \aleph \left(\mathrm{suc}\varnothing \right)$$
10		df-1o	$$⊢1_{𝑜}=\mathrm{suc}\varnothing$$
11	10	fveq2i	$$⊢\aleph \left(1_{𝑜}\right)=\aleph \left(\mathrm{suc}\varnothing \right)$$
12	11	breq2i	$$⊢ℝ\prec \aleph \left(1_{𝑜}\right)\leftrightarrow ℝ\prec \aleph \left(\mathrm{suc}\varnothing \right)$$
13	9 12	mtbir	$$⊢\neg ℝ\prec \aleph \left(1_{𝑜}\right)$$
14		fvex	$$⊢\aleph \left(1_{𝑜}\right)\in \mathrm{V}$$
15		reex	$$⊢ℝ\in \mathrm{V}$$
16		domtri	$$⊢\left(\aleph \left(1_{𝑜}\right)\in \mathrm{V}\wedge ℝ\in \mathrm{V}\right)\to \left(\aleph \left(1_{𝑜}\right)\preccurlyeq ℝ\leftrightarrow \neg ℝ\prec \aleph \left(1_{𝑜}\right)\right)$$
17	14 15 16	mp2an	$$⊢\aleph \left(1_{𝑜}\right)\preccurlyeq ℝ\leftrightarrow \neg ℝ\prec \aleph \left(1_{𝑜}\right)$$
18	13 17	mpbir	$$⊢\aleph \left(1_{𝑜}\right)\preccurlyeq ℝ$$