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 ∈ topGen ⁡ ran ⁡ .
2 retop ⊢ topGen ⁡ ran ⁡ . ∈ Top
3 ioossre ⊢ A B ⊆ ℝ
4 uniretop ⊢ ℝ = ⋃ topGen ⁡ ran ⁡ .
5 4 isopn3 ⊢ topGen ⁡ ran ⁡ . ∈ Top ∧ A B ⊆ ℝ → A B ∈ topGen ⁡ ran ⁡ . ↔ int ⁡ topGen ⁡ ran ⁡ . ⁡ A B = A B
6 2 3 5 mp2an ⊢ A B ∈ topGen ⁡ ran ⁡ . ↔ int ⁡ topGen ⁡ ran ⁡ . ⁡ A B = A B
7 1 6 mpbi ⊢ int ⁡ topGen ⁡ ran ⁡ . ⁡ A B = A B