This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )