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		tgioo4	⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
4	2 3	eqtr3i	⊢ ( ( ordTop ‘ ≤ ) ↾t ℝ ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )