Theorem qdensere2

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

	Ref	Expression
Hypotheses	remet.1	⊢ 𝐷 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
	tgioo.2	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion	qdensere2	⊢ ( ( cls ‘ 𝐽 ) ‘ ℚ ) = ℝ

Proof

Step	Hyp	Ref	Expression
1		remet.1	⊢ 𝐷 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
2		tgioo.2	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
3	1 2	tgioo	⊢ ( topGen ‘ ran (,) ) = 𝐽
4	3	fveq2i	⊢ ( cls ‘ ( topGen ‘ ran (,) ) ) = ( cls ‘ 𝐽 )
5	4	fveq1i	⊢ ( ( cls ‘ ( topGen ‘ ran (,) ) ) ‘ ℚ ) = ( ( cls ‘ 𝐽 ) ‘ ℚ )
6		qdensere	⊢ ( ( cls ‘ ( topGen ‘ ran (,) ) ) ‘ ℚ ) = ℝ
7	5 6	eqtr3i	⊢ ( ( cls ‘ 𝐽 ) ‘ ℚ ) = ℝ