Theorem retopn

Description: The topology of the real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019)

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

Proof

Step	Hyp	Ref	Expression
1		tgioo4	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ$$
2		df-refld	$$⊢{ℝ}_{\mathrm{fld}}={ℂ}_{\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}}\right)$$
5	1 4	eqtri	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℝ}_{\mathrm{fld}}\right)$$