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	|- QQ ~< RR

Proof

Step	Hyp	Ref	Expression
1		qnnen	|- QQ ~~ NN
2		ruc	|- NN ~< RR
3		ensdomtr	|- ( ( QQ ~~ NN /\ NN ~< RR ) -> QQ ~< RR )
4	1 2 3	mp2an	|- QQ ~< RR