Theorem mrcidm

Description: The closure operation is idempotent. (Contributed by Stefan O'Rear, 31-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		mrcfval.f	$$⊢F=\mathrm{mrCls}\left(C\right)$$
2	1	mrccl	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge U\subseteq X\right)\to F\left(U\right)\in C$$
3	1	mrcid	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge F\left(U\right)\in C\right)\to F\left(F\left(U\right)\right)=F\left(U\right)$$
4	2 3	syldan	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge U\subseteq X\right)\to F\left(F\left(U\right)\right)=F\left(U\right)$$