Metamath Proof Explorer

Theorem icccld

Description: Closed intervals are closed sets of the standard topology on RR . (Contributed by FL, 14-Sep-2007)

Ref Expression
Assertion icccld ⊢ A ∈ ℝ ∧ B ∈ ℝ → A B ∈ Clsd ⁡ topGen ⁡ ran ⁡ .

Proof

Step Hyp Ref Expression
1 difreicc ⊢ A ∈ ℝ ∧ B ∈ ℝ → ℝ ∖ A B = −∞ A ∪ B +∞
2 retop ⊢ topGen ⁡ ran ⁡ . ∈ Top
3 iooretop ⊢ −∞ A ∈ topGen ⁡ ran ⁡ .
4 iooretop ⊢ B +∞ ∈ topGen ⁡ ran ⁡ .
5 unopn ⊢ topGen ⁡ ran ⁡ . ∈ Top ∧ −∞ A ∈ topGen ⁡ ran ⁡ . ∧ B +∞ ∈ topGen ⁡ ran ⁡ . → −∞ A ∪ B +∞ ∈ topGen ⁡ ran ⁡ .
6 2 3 4 5 mp3an ⊢ −∞ A ∪ B +∞ ∈ topGen ⁡ ran ⁡ .
7 1 6 eqeltrdi ⊢ A ∈ ℝ ∧ B ∈ ℝ → ℝ ∖ A B ∈ topGen ⁡ ran ⁡ .
8 iccssre ⊢ A ∈ ℝ ∧ B ∈ ℝ → A B ⊆ ℝ
9 uniretop ⊢ ℝ = ⋃ topGen ⁡ ran ⁡ .
10 9 iscld2 ⊢ topGen ⁡ ran ⁡ . ∈ Top ∧ A B ⊆ ℝ → A B ∈ Clsd ⁡ topGen ⁡ ran ⁡ . ↔ ℝ ∖ A B ∈ topGen ⁡ ran ⁡ .
11 2 8 10 sylancr ⊢ A ∈ ℝ ∧ B ∈ ℝ → A B ∈ Clsd ⁡ topGen ⁡ ran ⁡ . ↔ ℝ ∖ A B ∈ topGen ⁡ ran ⁡ .
12 7 11 mpbird ⊢ A ∈ ℝ ∧ B ∈ ℝ → A B ∈ Clsd ⁡ topGen ⁡ ran ⁡ .