Theorem cldmre

Description: The closed sets of a topology comprise a Moore system on the points of the topology. (Contributed by Stefan O'Rear, 31-Jan-2015)

	Ref	Expression
Hypothesis	clscld.1	$$⊢X=\bigcup J$$
Assertion	cldmre	$$⊢J\in \mathrm{Top}\to \mathrm{Clsd}\left(J\right)\in \mathrm{Moore}\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		clscld.1	$$⊢X=\bigcup J$$
2	1	cldss2	$$⊢\mathrm{Clsd}\left(J\right)\subseteq 𝒫X$$
3	2	a1i	$$⊢J\in \mathrm{Top}\to \mathrm{Clsd}\left(J\right)\subseteq 𝒫X$$
4	1	topcld	$$⊢J\in \mathrm{Top}\to X\in \mathrm{Clsd}\left(J\right)$$
5		intcld	$$⊢\left(x\ne \varnothing \wedge x\subseteq \mathrm{Clsd}\left(J\right)\right)\to \bigcap x\in \mathrm{Clsd}\left(J\right)$$
6	5	ancoms	$$⊢\left(x\subseteq \mathrm{Clsd}\left(J\right)\wedge x\ne \varnothing \right)\to \bigcap x\in \mathrm{Clsd}\left(J\right)$$
7	6	3adant1	$$⊢\left(J\in \mathrm{Top}\wedge x\subseteq \mathrm{Clsd}\left(J\right)\wedge x\ne \varnothing \right)\to \bigcap x\in \mathrm{Clsd}\left(J\right)$$
8	3 4 7	ismred	$$⊢J\in \mathrm{Top}\to \mathrm{Clsd}\left(J\right)\in \mathrm{Moore}\left(X\right)$$