# 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}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
Assertion tgioo2 ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)={J}{↾}_{𝑡}ℝ$

### Proof

Step Hyp Ref Expression
1 tgioo2.1 ${⊢}{J}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
2 eqid ${⊢}{\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}={\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}$
3 cnxmet ${⊢}\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)$
4 ax-resscn ${⊢}ℝ\subseteq ℂ$
5 1 cnfldtopn ${⊢}{J}=\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)$
6 eqid ${⊢}\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)$
7 2 5 6 metrest ${⊢}\left(\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)\wedge ℝ\subseteq ℂ\right)\to {J}{↾}_{𝑡}ℝ=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)$
8 3 4 7 mp2an ${⊢}{J}{↾}_{𝑡}ℝ=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)$
9 2 8 tgioo ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)={J}{↾}_{𝑡}ℝ$