Theorem xrtgcntopre

Description: The standard topologies on the extended reals and on the complex numbers, coincide when restricted to the reals. (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Assertion	xrtgcntopre	$$⊢\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}ℝ=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}ℝ=\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}ℝ$$
2	1	xrtgioo	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}ℝ$$
3		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
4	3	tgioo2	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ$$
5	2 4	eqtr3i	$$⊢\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}ℝ=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ$$