This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qdensere2

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

Ref Expression
Hypotheses remet.1 ⊢ D = abs ∘ − ↾ ℝ 2
tgioo.2 ⊢ J = MetOpen ⁡ D
Assertion qdensere2 ⊢ cls ⁡ J ⁡ ℚ = ℝ

Proof

Step Hyp Ref Expression
1 remet.1 ⊢ D = abs ∘ − ↾ ℝ 2
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 ⁡ . ⁡ ℚ = cls ⁡ J ⁡ ℚ
6 qdensere ⊢ cls ⁡ topGen ⁡ ran ⁡ . ⁡ ℚ = ℝ
7 5 6 eqtr3i ⊢ cls ⁡ J ⁡ ℚ = ℝ