Metamath Proof Explorer


Theorem qdensere2

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

Ref Expression
Hypotheses remet.1 D=abs2
tgioo.2 J=MetOpenD
Assertion qdensere2 clsJ=

Proof

Step Hyp Ref Expression
1 remet.1 D=abs2
2 tgioo.2 J=MetOpenD
3 1 2 tgioo topGenran.=J
4 3 fveq2i clstopGenran.=clsJ
5 4 fveq1i clstopGenran.=clsJ
6 qdensere clstopGenran.=
7 5 6 eqtr3i clsJ=