Theorem qdensere2

Description: QQ is dense in RR . (Contributed by NM, 24-Aug-2007)

	Ref	Expression
Hypotheses	remet.1	|- D = ( ( abs o. - ) |` ( RR X. RR ) )
	tgioo.2	|- J = ( MetOpen ` D )
Assertion	qdensere2	|- ( ( cls ` J ) ` QQ ) = RR

Proof

Step	Hyp	Ref	Expression
1		remet.1	|- D = ( ( abs o. - ) |` ( RR X. RR ) )
2		tgioo.2	|- J = ( MetOpen ` D )
3	1 2	tgioo	|- ( topGen ` ran (,) ) = J
4	3	fveq2i	|- ( cls ` ( topGen ` ran (,) ) ) = ( cls ` J )
5	4	fveq1i	|- ( ( cls ` ( topGen ` ran (,) ) ) ` QQ ) = ( ( cls ` J ) ` QQ )
6		qdensere	|- ( ( cls ` ( topGen ` ran (,) ) ) ` QQ ) = RR
7	5 6	eqtr3i	|- ( ( cls ` J ) ` QQ ) = RR