Theorem sncldre

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

Proof

Step	Hyp	Ref	Expression
1		rehaus	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Haus}$$
2		uniretop	$$⊢ℝ=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
3	2	sncld	$$⊢\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Haus}\wedge A\in ℝ\right)\to \left\{A\right\}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
4	1 3	mpan	$$⊢A\in ℝ\to \left\{A\right\}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$