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 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
Assertion tgioo2 ( topGen ‘ ran (,) ) = ( 𝐽 ↾t ℝ )

Proof

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