Theorem tgioo3

Description: The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Mario Carneiro, 13-Aug-2014) (Revised by Thierry Arnoux, 3-Jul-2019)

	Ref	Expression
Hypothesis	tgioo3.1	$$⊢J=\mathrm{TopOpen}\left({ℝ}_{\mathrm{fld}}\right)$$
Assertion	tgioo3	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=J$$

Proof

Step	Hyp	Ref	Expression
1		tgioo3.1	$$⊢J=\mathrm{TopOpen}\left({ℝ}_{\mathrm{fld}}\right)$$
2		eqid	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ$$
3		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
4	2 3	resstopn	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right)$$
5		tgioo4	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ$$
6		df-refld	$$⊢{ℝ}_{\mathrm{fld}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ$$
7	6	fveq2i	$$⊢\mathrm{TopOpen}\left({ℝ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right)$$
8	1 7	eqtri	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right)$$
9	4 5 8	3eqtr4i	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=J$$