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 (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 (,) 𝐵 )

Proof

Step Hyp Ref Expression
1 iooretop ⊢ ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) )
2 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
3 ioossre ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
4 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
5 4 isopn3 ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℝ ) → ( ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) ) ↔ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) ) )
6 2 3 5 mp2an ⊢ ( ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) ) ↔ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
7 1 6 mpbi ⊢ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 (,) 𝐵 )