Theorem cldmreon

Description: The closed sets of a topology over a set are a Moore collection over the same set. (Contributed by Stefan O'Rear, 31-Jan-2015)

	Ref	Expression
Assertion	cldmreon	$$⊢J\in \mathrm{TopOn}\left(B\right)\to \mathrm{Clsd}\left(J\right)\in \mathrm{Moore}\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		topontop	$$⊢J\in \mathrm{TopOn}\left(B\right)\to J\in \mathrm{Top}$$
2		eqid	$$⊢\bigcup J=\bigcup J$$
3	2	cldmre	$$⊢J\in \mathrm{Top}\to \mathrm{Clsd}\left(J\right)\in \mathrm{Moore}\left(\bigcup J\right)$$
4	1 3	syl	$$⊢J\in \mathrm{TopOn}\left(B\right)\to \mathrm{Clsd}\left(J\right)\in \mathrm{Moore}\left(\bigcup J\right)$$
5		toponuni	$$⊢J\in \mathrm{TopOn}\left(B\right)\to B=\bigcup J$$
6	5	fveq2d	$$⊢J\in \mathrm{TopOn}\left(B\right)\to \mathrm{Moore}\left(B\right)=\mathrm{Moore}\left(\bigcup J\right)$$
7	4 6	eleqtrrd	$$⊢J\in \mathrm{TopOn}\left(B\right)\to \mathrm{Clsd}\left(J\right)\in \mathrm{Moore}\left(B\right)$$