Theorem qdensere2

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

	Ref	Expression
Hypotheses	remet.1	$$⊢D={\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}$$
	tgioo.2	$$⊢J=\mathrm{MetOpen}\left(D\right)$$
Assertion	qdensere2	$$⊢\mathrm{cls}\left(J\right)\left(\mathbb{Q}\right)=ℝ$$

Proof

Step	Hyp	Ref	Expression
1		remet.1	$$⊢D={\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}$$
2		tgioo.2	$$⊢J=\mathrm{MetOpen}\left(D\right)$$
3	1 2	tgioo	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=J$$
4	3	fveq2i	$$⊢\mathrm{cls}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)=\mathrm{cls}\left(J\right)$$
5	4	fveq1i	$$⊢\mathrm{cls}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\mathbb{Q}\right)=\mathrm{cls}\left(J\right)\left(\mathbb{Q}\right)$$
6		qdensere	$$⊢\mathrm{cls}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\mathbb{Q}\right)=ℝ$$
7	5 6	eqtr3i	$$⊢\mathrm{cls}\left(J\right)\left(\mathbb{Q}\right)=ℝ$$