# 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 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left[{A},{B}\right]\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 difreicc ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to ℝ\setminus \left[{A},{B}\right]=\left(\mathrm{-\infty },{A}\right)\cup \left({B},\mathrm{+\infty }\right)$
2 retop ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$
3 iooretop ${⊢}\left(\mathrm{-\infty },{A}\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
4 iooretop ${⊢}\left({B},\mathrm{+\infty }\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
5 unopn ${⊢}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}\wedge \left(\mathrm{-\infty },{A}\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\wedge \left({B},\mathrm{+\infty }\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\to \left(\mathrm{-\infty },{A}\right)\cup \left({B},\mathrm{+\infty }\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
6 2 3 4 5 mp3an ${⊢}\left(\mathrm{-\infty },{A}\right)\cup \left({B},\mathrm{+\infty }\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
7 1 6 eqeltrdi ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to ℝ\setminus \left[{A},{B}\right]\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
8 iccssre ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left[{A},{B}\right]\subseteq ℝ$
9 uniretop ${⊢}ℝ=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
10 9 iscld2 ${⊢}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}\wedge \left[{A},{B}\right]\subseteq ℝ\right)\to \left(\left[{A},{B}\right]\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)↔ℝ\setminus \left[{A},{B}\right]\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$
11 2 8 10 sylancr ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(\left[{A},{B}\right]\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)↔ℝ\setminus \left[{A},{B}\right]\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$
12 7 11 mpbird ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left[{A},{B}\right]\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$