Theorem resdomq

Description: The set of rationals is strictly less equinumerous than the set of reals ( RR strictly dominates QQ ). (Contributed by NM, 18-Dec-2004)

	Ref	Expression
Assertion	resdomq	$$⊢\mathbb{Q}\prec ℝ$$

Proof

Step	Hyp	Ref	Expression
1		qnnen	$$⊢\mathbb{Q}\approx \mathbb{N}$$
2		ruc	$$⊢\mathbb{N}\prec ℝ$$
3		ensdomtr	$$⊢\left(\mathbb{Q}\approx \mathbb{N}\wedge \mathbb{N}\prec ℝ\right)\to \mathbb{Q}\prec ℝ$$
4	1 2 3	mp2an	$$⊢\mathbb{Q}\prec ℝ$$