Theorem ioontr

Description: The interior of an interval in the standard topology on RR is the open interval itself. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	ioontr	|- ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = ( A (,) B )

Proof

Step	Hyp	Ref	Expression
1		iooretop	|- ( A (,) B ) e. ( topGen ` ran (,) )
2		retop	|- ( topGen ` ran (,) ) e. Top
3		ioossre	|- ( A (,) B ) C_ RR
4		uniretop	|- RR = U. ( topGen ` ran (,) )
5	4	isopn3	|- ( ( ( topGen ` ran (,) ) e. Top /\ ( A (,) B ) C_ RR ) -> ( ( A (,) B ) e. ( topGen ` ran (,) ) <-> ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = ( A (,) B ) ) )
6	2 3 5	mp2an	|- ( ( A (,) B ) e. ( topGen ` ran (,) ) <-> ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = ( A (,) B ) )
7	1 6	mpbi	|- ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = ( A (,) B )