Theorem mrccls

Description: Moore closure generalizes closure in a topology. (Contributed by Stefan O'Rear, 31-Jan-2015)

	Ref	Expression
Hypothesis	mrccls.f	$$⊢F=\mathrm{mrCls}\left(\mathrm{Clsd}\left(J\right)\right)$$
Assertion	mrccls	$$⊢J\in \mathrm{Top}\to \mathrm{cls}\left(J\right)=F$$

Proof

Step	Hyp	Ref	Expression
1		mrccls.f	$$⊢F=\mathrm{mrCls}\left(\mathrm{Clsd}\left(J\right)\right)$$
2		eqid	$$⊢\bigcup J=\bigcup J$$
3	2	clsfval	$$⊢J\in \mathrm{Top}\to \mathrm{cls}\left(J\right)=\left(a\in 𝒫\bigcup J⟼\bigcap \left\{b\in \mathrm{Clsd}\left(J\right)|a\subseteq b\right\}\right)$$
4	2	cldmre	$$⊢J\in \mathrm{Top}\to \mathrm{Clsd}\left(J\right)\in \mathrm{Moore}\left(\bigcup J\right)$$
5	1	mrcfval	$$⊢\mathrm{Clsd}\left(J\right)\in \mathrm{Moore}\left(\bigcup J\right)\to F=\left(a\in 𝒫\bigcup J⟼\bigcap \left\{b\in \mathrm{Clsd}\left(J\right)|a\subseteq b\right\}\right)$$
6	4 5	syl	$$⊢J\in \mathrm{Top}\to F=\left(a\in 𝒫\bigcup J⟼\bigcap \left\{b\in \mathrm{Clsd}\left(J\right)|a\subseteq b\right\}\right)$$
7	3 6	eqtr4d	$$⊢J\in \mathrm{Top}\to \mathrm{cls}\left(J\right)=F$$