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 ℝ )