Theorem mrcflem

Description: The domain and codomain of the function expression for Moore closures. (Contributed by Stefan O'Rear, 31-Jan-2015)

	Ref	Expression
Assertion	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$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge x\in 𝒫X\right)\to C\in \mathrm{Moore}\left(X\right)$$
2		ssrab2	$$⊢\left\{s\in C|x\subseteq s\right\}\subseteq C$$
3	2	a1i	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge x\in 𝒫X\right)\to \left\{s\in C|x\subseteq s\right\}\subseteq C$$
4		sseq2	$$⊢s=X\to \left(x\subseteq s\leftrightarrow x\subseteq X\right)$$
5		mre1cl	$$⊢C\in \mathrm{Moore}\left(X\right)\to X\in C$$
6	5	adantr	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge x\in 𝒫X\right)\to X\in C$$
7		elpwi	$$⊢x\in 𝒫X\to x\subseteq X$$
8	7	adantl	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge x\in 𝒫X\right)\to x\subseteq X$$
9	4 6 8	elrabd	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge x\in 𝒫X\right)\to X\in \left\{s\in C|x\subseteq s\right\}$$
10	9	ne0d	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge x\in 𝒫X\right)\to \left\{s\in C|x\subseteq s\right\}\ne \varnothing$$
11		mreintcl	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge \left\{s\in C|x\subseteq s\right\}\subseteq C\wedge \left\{s\in C|x\subseteq s\right\}\ne \varnothing \right)\to \bigcap \left\{s\in C|x\subseteq s\right\}\in C$$
12	1 3 10 11	syl3anc	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge x\in 𝒫X\right)\to \bigcap \left\{s\in C|x\subseteq s\right\}\in C$$
13	12	fmpttd	$$⊢C\in \mathrm{Moore}\left(X\right)\to \left(x\in 𝒫X⟼\bigcap \left\{s\in C|x\subseteq s\right\}\right):𝒫X⟶C$$