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

Metamath Proof Explorer

Theorem tgioo4

Description: The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Assertion tgioo4 ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
2 1 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )