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	⊢ ( ( ordTop ‘ ≤ ) ↾t ℝ ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( ( ordTop ‘ ≤ ) ↾t ℝ ) = ( ( ordTop ‘ ≤ ) ↾t ℝ )
2	1	xrtgioo	⊢ ( topGen ‘ ran (,) ) = ( ( ordTop ‘ ≤ ) ↾t ℝ )
3		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
4	3	tgioo2	⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
5	2 4	eqtr3i	⊢ ( ( ordTop ‘ ≤ ) ↾t ℝ ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )