Theorem mrccl

Description: The Moore closure of a set is a closed set. (Contributed by Stefan O'Rear, 31-Jan-2015)

	Ref	Expression
Hypothesis	mrcfval.f	$$⊢F=\mathrm{mrCls}\left(C\right)$$
Assertion	mrccl	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge U\subseteq X\right)\to F\left(U\right)\in C$$

Proof

Step	Hyp	Ref	Expression
1		mrcfval.f	$$⊢F=\mathrm{mrCls}\left(C\right)$$
2	1	mrcf	$$⊢C\in \mathrm{Moore}\left(X\right)\to F:𝒫X⟶C$$
3	2	adantr	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge U\subseteq X\right)\to F:𝒫X⟶C$$
4		mre1cl	$$⊢C\in \mathrm{Moore}\left(X\right)\to X\in C$$
5		elpw2g	$$⊢X\in C\to \left(U\in 𝒫X\leftrightarrow U\subseteq X\right)$$
6	4 5	syl	$$⊢C\in \mathrm{Moore}\left(X\right)\to \left(U\in 𝒫X\leftrightarrow U\subseteq X\right)$$
7	6	biimpar	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge U\subseteq X\right)\to U\in 𝒫X$$
8	3 7	ffvelrnd	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge U\subseteq X\right)\to F\left(U\right)\in C$$