Theorem mrcid

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

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

Proof

Step	Hyp	Ref	Expression
1		mrcfval.f	$$⊢F=\mathrm{mrCls}\left(C\right)$$
2		mress	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge U\in C\right)\to U\subseteq X$$
3	1	mrcval	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge U\subseteq X\right)\to F\left(U\right)=\bigcap \left\{s\in C|U\subseteq s\right\}$$
4	2 3	syldan	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge U\in C\right)\to F\left(U\right)=\bigcap \left\{s\in C|U\subseteq s\right\}$$
5		intmin	$$⊢U\in C\to \bigcap \left\{s\in C|U\subseteq s\right\}=U$$
6	5	adantl	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge U\in C\right)\to \bigcap \left\{s\in C|U\subseteq s\right\}=U$$
7	4 6	eqtrd	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge U\in C\right)\to F\left(U\right)=U$$