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 RR ) = ( ( TopOpen ` CCfld ) |`t RR )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( ( ordTop ` <_ ) |`t RR ) = ( ( ordTop ` <_ ) |`t RR )
2	1	xrtgioo	|- ( topGen ` ran (,) ) = ( ( ordTop ` <_ ) |`t RR )
3		tgioo4	|- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
4	2 3	eqtr3i	|- ( ( ordTop ` <_ ) |`t RR ) = ( ( TopOpen ` CCfld ) |`t RR )