Theorem fnmrc

Description: Moore-closure is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015)

	Ref	Expression
Assertion	fnmrc	$$⊢\mathrm{mrCls}Fn\bigcup \mathrm{ran}\mathrm{Moore}$$

Proof

Step	Hyp	Ref	Expression
1		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)$$
2	1	fnmpt	$$⊢\forall c\in \bigcup \mathrm{ran}\mathrm{Moore}\left(x\in 𝒫\bigcup c⟼\bigcap \left\{s\in c|x\subseteq s\right\}\right)\in \mathrm{V}\to \mathrm{mrCls}Fn\bigcup \mathrm{ran}\mathrm{Moore}$$
3		mreunirn	$$⊢c\in \bigcup \mathrm{ran}\mathrm{Moore}\leftrightarrow c\in \mathrm{Moore}\left(\bigcup c\right)$$
4		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$$
5		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$$
6	4 5	syl	$$⊢c\in \mathrm{Moore}\left(\bigcup c\right)\to \left(x\in 𝒫\bigcup c⟼\bigcap \left\{s\in c|x\subseteq s\right\}\right)\subseteq 𝒫\bigcup c\times c$$
7		vuniex	$$⊢\bigcup c\in \mathrm{V}$$
8	7	pwex	$$⊢𝒫\bigcup c\in \mathrm{V}$$
9		vex	$$⊢c\in \mathrm{V}$$
10	8 9	xpex	$$⊢𝒫\bigcup c\times c\in \mathrm{V}$$
11		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}$$
12	6 10 11	sylancl	$$⊢c\in \mathrm{Moore}\left(\bigcup c\right)\to \left(x\in 𝒫\bigcup c⟼\bigcap \left\{s\in c|x\subseteq s\right\}\right)\in \mathrm{V}$$
13	3 12	sylbi	$$⊢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}$$
14	2 13	mprg	$$⊢\mathrm{mrCls}Fn\bigcup \mathrm{ran}\mathrm{Moore}$$