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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )

Proof

Step Hyp Ref Expression
1 difreicc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) = ( ( -∞ (,) 𝐴 ) ∪ ( 𝐵 (,) +∞ ) ) )
2 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
3 iooretop ⊢ ( -∞ (,) 𝐴 ) ∈ ( topGen ‘ ran (,) )
4 iooretop ⊢ ( 𝐵 (,) +∞ ) ∈ ( topGen ‘ ran (,) )
5 unopn ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( -∞ (,) 𝐴 ) ∈ ( topGen ‘ ran (,) ) ∧ ( 𝐵 (,) +∞ ) ∈ ( topGen ‘ ran (,) ) ) → ( ( -∞ (,) 𝐴 ) ∪ ( 𝐵 (,) +∞ ) ) ∈ ( topGen ‘ ran (,) ) )
6 2 3 4 5 mp3an ⊢ ( ( -∞ (,) 𝐴 ) ∪ ( 𝐵 (,) +∞ ) ) ∈ ( topGen ‘ ran (,) )
7 1 6 eqeltrdi ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ∈ ( topGen ‘ ran (,) ) )
8 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
9 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
10 9 iscld2 ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℝ ) → ( ( 𝐴 [,] 𝐵 ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) ↔ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ∈ ( topGen ‘ ran (,) ) ) )
11 2 8 10 sylancr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 [,] 𝐵 ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) ↔ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ∈ ( topGen ‘ ran (,) ) ) )
12 7 11 mpbird ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )