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	⊢ ℚ ≺ ℝ

Proof

Step	Hyp	Ref	Expression
1		qnnen	⊢ ℚ ≈ ℕ
2		ruc	⊢ ℕ ≺ ℝ
3		ensdomtr	⊢ ( ( ℚ ≈ ℕ ∧ ℕ ≺ ℝ ) → ℚ ≺ ℝ )
4	1 2 3	mp2an	⊢ ℚ ≺ ℝ