Theorem aleph1irr

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

	Ref	Expression
Assertion	aleph1irr	$$⊢\aleph \left(1_{𝑜}\right)\preccurlyeq \left(ℝ\setminus \mathbb{Q}\right)$$

Proof

Step	Hyp	Ref	Expression
1		aleph1re	$$⊢\aleph \left(1_{𝑜}\right)\preccurlyeq ℝ$$
2		reex	$$⊢ℝ\in \mathrm{V}$$
3		numth3	$$⊢ℝ\in \mathrm{V}\to ℝ\in \mathrm{dom}\mathrm{card}$$
4	2 3	ax-mp	$$⊢ℝ\in \mathrm{dom}\mathrm{card}$$
5		nnenom	$$⊢\mathbb{N}\approx \mathrm{\omega }$$
6	5	ensymi	$$⊢\mathrm{\omega }\approx \mathbb{N}$$
7		ruc	$$⊢\mathbb{N}\prec ℝ$$
8		ensdomtr	$$⊢\left(\mathrm{\omega }\approx \mathbb{N}\wedge \mathbb{N}\prec ℝ\right)\to \mathrm{\omega }\prec ℝ$$
9	6 7 8	mp2an	$$⊢\mathrm{\omega }\prec ℝ$$
10		sdomdom	$$⊢\mathrm{\omega }\prec ℝ\to \mathrm{\omega }\preccurlyeq ℝ$$
11	9 10	ax-mp	$$⊢\mathrm{\omega }\preccurlyeq ℝ$$
12		resdomq	$$⊢\mathbb{Q}\prec ℝ$$
13		infdif	$$⊢\left(ℝ\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq ℝ\wedge \mathbb{Q}\prec ℝ\right)\to \left(ℝ\setminus \mathbb{Q}\right)\approx ℝ$$
14	4 11 12 13	mp3an	$$⊢\left(ℝ\setminus \mathbb{Q}\right)\approx ℝ$$
15	14	ensymi	$$⊢ℝ\approx \left(ℝ\setminus \mathbb{Q}\right)$$
16		domentr	$$⊢\left(\aleph \left(1_{𝑜}\right)\preccurlyeq ℝ\wedge ℝ\approx \left(ℝ\setminus \mathbb{Q}\right)\right)\to \aleph \left(1_{𝑜}\right)\preccurlyeq \left(ℝ\setminus \mathbb{Q}\right)$$
17	1 15 16	mp2an	$$⊢\aleph \left(1_{𝑜}\right)\preccurlyeq \left(ℝ\setminus \mathbb{Q}\right)$$