Theorem mrcfval

Description: Value of the function expression for the Moore closure. (Contributed by Stefan O'Rear, 31-Jan-2015)

	Ref	Expression
Hypothesis	mrcfval.f	$$⊢F=\mathrm{mrCls}\left(C\right)$$
Assertion	mrcfval	$$⊢C\in \mathrm{Moore}\left(X\right)\to F=\left(x\in 𝒫X⟼\bigcap \left\{s\in C|x\subseteq s\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		mrcfval.f	$$⊢F=\mathrm{mrCls}\left(C\right)$$
2		fvssunirn	$$⊢\mathrm{Moore}\left(X\right)\subseteq \bigcup \mathrm{ran}\mathrm{Moore}$$
3	2	sseli	$$⊢C\in \mathrm{Moore}\left(X\right)\to C\in \bigcup \mathrm{ran}\mathrm{Moore}$$
4		unieq	$$⊢c=C\to \bigcup c=\bigcup C$$
5	4	pweqd	$$⊢c=C\to 𝒫\bigcup c=𝒫\bigcup C$$
6		rabeq	$$⊢c=C\to \left\{s\in c|x\subseteq s\right\}=\left\{s\in C|x\subseteq s\right\}$$
7	6	inteqd	$$⊢c=C\to \bigcap \left\{s\in c|x\subseteq s\right\}=\bigcap \left\{s\in C|x\subseteq s\right\}$$
8	5 7	mpteq12dv	$$⊢c=C\to \left(x\in 𝒫\bigcup c⟼\bigcap \left\{s\in c|x\subseteq s\right\}\right)=\left(x\in 𝒫\bigcup C⟼\bigcap \left\{s\in C|x\subseteq s\right\}\right)$$
9		df-mrc	$$⊢\mathrm{mrCls}=\left(c\in \bigcup \mathrm{ran}\mathrm{Moore}⟼\left(x\in 𝒫\bigcup c⟼\bigcap \left\{s\in c|x\subseteq s\right\}\right)\right)$$
10		mreunirn	$$⊢c\in \bigcup \mathrm{ran}\mathrm{Moore}\leftrightarrow c\in \mathrm{Moore}\left(\bigcup c\right)$$
11		mrcflem	$$⊢c\in \mathrm{Moore}\left(\bigcup c\right)\to \left(x\in 𝒫\bigcup c⟼\bigcap \left\{s\in c|x\subseteq s\right\}\right):𝒫\bigcup c⟶c$$
12	10 11	sylbi	$$⊢c\in \bigcup \mathrm{ran}\mathrm{Moore}\to \left(x\in 𝒫\bigcup c⟼\bigcap \left\{s\in c|x\subseteq s\right\}\right):𝒫\bigcup c⟶c$$
13		fssxp	$$⊢\left(x\in 𝒫\bigcup c⟼\bigcap \left\{s\in c|x\subseteq s\right\}\right):𝒫\bigcup c⟶c\to \left(x\in 𝒫\bigcup c⟼\bigcap \left\{s\in c|x\subseteq s\right\}\right)\subseteq 𝒫\bigcup c\times c$$
14	12 13	syl	$$⊢c\in \bigcup \mathrm{ran}\mathrm{Moore}\to \left(x\in 𝒫\bigcup c⟼\bigcap \left\{s\in c|x\subseteq s\right\}\right)\subseteq 𝒫\bigcup c\times c$$
15		vuniex	$$⊢\bigcup c\in \mathrm{V}$$
16	15	pwex	$$⊢𝒫\bigcup c\in \mathrm{V}$$
17		vex	$$⊢c\in \mathrm{V}$$
18	16 17	xpex	$$⊢𝒫\bigcup c\times c\in \mathrm{V}$$
19		ssexg	$$⊢\left(\left(x\in 𝒫\bigcup c⟼\bigcap \left\{s\in c|x\subseteq s\right\}\right)\subseteq 𝒫\bigcup c\times c\wedge 𝒫\bigcup c\times c\in \mathrm{V}\right)\to \left(x\in 𝒫\bigcup c⟼\bigcap \left\{s\in c|x\subseteq s\right\}\right)\in \mathrm{V}$$
20	14 18 19	sylancl	$$⊢c\in \bigcup \mathrm{ran}\mathrm{Moore}\to \left(x\in 𝒫\bigcup c⟼\bigcap \left\{s\in c|x\subseteq s\right\}\right)\in \mathrm{V}$$
21	8 9 20	fvmpt3	$$⊢C\in \bigcup \mathrm{ran}\mathrm{Moore}\to \mathrm{mrCls}\left(C\right)=\left(x\in 𝒫\bigcup C⟼\bigcap \left\{s\in C|x\subseteq s\right\}\right)$$
22	3 21	syl	$$⊢C\in \mathrm{Moore}\left(X\right)\to \mathrm{mrCls}\left(C\right)=\left(x\in 𝒫\bigcup C⟼\bigcap \left\{s\in C|x\subseteq s\right\}\right)$$
23		mreuni	$$⊢C\in \mathrm{Moore}\left(X\right)\to \bigcup C=X$$
24	23	pweqd	$$⊢C\in \mathrm{Moore}\left(X\right)\to 𝒫\bigcup C=𝒫X$$
25	24	mpteq1d	$$⊢C\in \mathrm{Moore}\left(X\right)\to \left(x\in 𝒫\bigcup C⟼\bigcap \left\{s\in C|x\subseteq s\right\}\right)=\left(x\in 𝒫X⟼\bigcap \left\{s\in C|x\subseteq s\right\}\right)$$
26	22 25	eqtrd	$$⊢C\in \mathrm{Moore}\left(X\right)\to \mathrm{mrCls}\left(C\right)=\left(x\in 𝒫X⟼\bigcap \left\{s\in C|x\subseteq s\right\}\right)$$
27	1 26	syl5eq	$$⊢C\in \mathrm{Moore}\left(X\right)\to F=\left(x\in 𝒫X⟼\bigcap \left\{s\in C|x\subseteq s\right\}\right)$$