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		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
2	1	tgioo2	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ$$
3		df-refld	$$⊢{ℝ}_{\mathrm{fld}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ$$
4	3 1	resstopn	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ=\mathrm{TopOpen}\left({ℝ}_{\mathrm{fld}}\right)$$
5	2 4	eqtri	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℝ}_{\mathrm{fld}}\right)$$