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		eqid	|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
4	3	tgioo2	|- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
5	2 4	eqtr3i	|- ( ( ordTop ` <_ ) |`t RR ) = ( ( TopOpen ` CCfld ) |`t RR )