Theorem t1sncld

Description: In a T_1 space, singletons are closed. (Contributed by Jeff Hankins, 1-Feb-2010)

	Ref	Expression
Hypothesis	ist0.1	$$⊢X=\bigcup J$$
Assertion	t1sncld	$$⊢\left(J\in \mathrm{Fre}\wedge A\in X\right)\to \left\{A\right\}\in \mathrm{Clsd}\left(J\right)$$

Proof

Step	Hyp	Ref	Expression
1		ist0.1	$$⊢X=\bigcup J$$
2	1	ist1	$$⊢J\in \mathrm{Fre}\leftrightarrow \left(J\in \mathrm{Top}\wedge \forall x\in X\left\{x\right\}\in \mathrm{Clsd}\left(J\right)\right)$$
3		sneq	$$⊢x=A\to \left\{x\right\}=\left\{A\right\}$$
4	3	eleq1d	$$⊢x=A\to \left(\left\{x\right\}\in \mathrm{Clsd}\left(J\right)\leftrightarrow \left\{A\right\}\in \mathrm{Clsd}\left(J\right)\right)$$
5	4	rspccv	$$⊢\forall x\in X\left\{x\right\}\in \mathrm{Clsd}\left(J\right)\to \left(A\in X\to \left\{A\right\}\in \mathrm{Clsd}\left(J\right)\right)$$
6	2 5	simplbiim	$$⊢J\in \mathrm{Fre}\to \left(A\in X\to \left\{A\right\}\in \mathrm{Clsd}\left(J\right)\right)$$
7	6	imp	$$⊢\left(J\in \mathrm{Fre}\wedge A\in X\right)\to \left\{A\right\}\in \mathrm{Clsd}\left(J\right)$$