Theorem sncld

Description: A singleton is closed in a Hausdorff space. (Contributed by NM, 5-Mar-2007) (Revised by Mario Carneiro, 24-Aug-2015)

	Ref	Expression
Hypothesis	t1sep.1	$$⊢X=\bigcup J$$
Assertion	sncld	$$⊢\left(J\in \mathrm{Haus}\wedge P\in X\right)\to \left\{P\right\}\in \mathrm{Clsd}\left(J\right)$$

Proof

Step	Hyp	Ref	Expression
1		t1sep.1	$$⊢X=\bigcup J$$
2		haust1	$$⊢J\in \mathrm{Haus}\to J\in \mathrm{Fre}$$
3	1	t1sncld	$$⊢\left(J\in \mathrm{Fre}\wedge P\in X\right)\to \left\{P\right\}\in \mathrm{Clsd}\left(J\right)$$
4	2 3	sylan	$$⊢\left(J\in \mathrm{Haus}\wedge P\in X\right)\to \left\{P\right\}\in \mathrm{Clsd}\left(J\right)$$