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