Description: A singleton is closed w.r.t. the standard topology on the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | sncldre | ⊢ ( 𝐴 ∈ ℝ → { 𝐴 } ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rehaus | ⊢ ( topGen ‘ ran (,) ) ∈ Haus | |
2 | uniretop | ⊢ ℝ = ∪ ( topGen ‘ ran (,) ) | |
3 | 2 | sncld | ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Haus ∧ 𝐴 ∈ ℝ ) → { 𝐴 } ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) ) |
4 | 1 3 | mpan | ⊢ ( 𝐴 ∈ ℝ → { 𝐴 } ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) ) |