Theorem mrcf

Description: The Moore closure is a function mapping arbitrary subsets to closed sets. (Contributed by Stefan O'Rear, 31-Jan-2015)

	Ref	Expression
Hypothesis	mrcfval.f	$$⊢F=\mathrm{mrCls}\left(C\right)$$
Assertion	mrcf	$$⊢C\in \mathrm{Moore}\left(X\right)\to F:𝒫X⟶C$$

Proof

Step	Hyp	Ref	Expression
1		mrcfval.f	$$⊢F=\mathrm{mrCls}\left(C\right)$$
2		mrcflem	$$⊢C\in \mathrm{Moore}\left(X\right)\to \left(x\in 𝒫X⟼\bigcap \left\{s\in C|x\subseteq s\right\}\right):𝒫X⟶C$$
3	1	mrcfval	$$⊢C\in \mathrm{Moore}\left(X\right)\to F=\left(x\in 𝒫X⟼\bigcap \left\{s\in C|x\subseteq s\right\}\right)$$
4	3	feq1d	$$⊢C\in \mathrm{Moore}\left(X\right)\to \left(F:𝒫X⟶C\leftrightarrow \left(x\in 𝒫X⟼\bigcap \left\{s\in C|x\subseteq s\right\}\right):𝒫X⟶C\right)$$
5	2 4	mpbird	$$⊢C\in \mathrm{Moore}\left(X\right)\to F:𝒫X⟶C$$