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

Metamath Proof Explorer

Theorem tgioo2

Description: The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Mario Carneiro, 13-Aug-2014)

Ref Expression
Hypothesis tgioo2.1 ⊢ J = TopOpen ⁡ ℂ fld
Assertion tgioo2 ⊢ topGen ⁡ ran ⁡ . = J ↾ 𝑡 ℝ

Proof

Step Hyp Ref Expression
1 tgioo2.1 ⊢ J = TopOpen ⁡ ℂ fld
2 eqid ⊢ abs ∘ − ↾ ℝ 2 = abs ∘ − ↾ ℝ 2
3 cnxmet ⊢ abs ∘ − ∈ ∞Met ⁡ ℂ
4 ax-resscn ⊢ ℝ ⊆ ℂ
5 1 cnfldtopn ⊢ J = MetOpen ⁡ abs ∘ −
6 eqid ⊢ MetOpen ⁡ abs ∘ − ↾ ℝ 2 = MetOpen ⁡ abs ∘ − ↾ ℝ 2
7 2 5 6 metrest ⊢ abs ∘ − ∈ ∞Met ⁡ ℂ ∧ ℝ ⊆ ℂ → J ↾ 𝑡 ℝ = MetOpen ⁡ abs ∘ − ↾ ℝ 2
8 3 4 7 mp2an ⊢ J ↾ 𝑡 ℝ = MetOpen ⁡ abs ∘ − ↾ ℝ 2
9 2 8 tgioo ⊢ topGen ⁡ ran ⁡ . = J ↾ 𝑡 ℝ