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{\upharpoonright }_{𝑡}ℝ$$

Proof

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