Theorem mrcssid

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

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

Proof

Step	Hyp	Ref	Expression
1		mrcfval.f	$$⊢F=\mathrm{mrCls}\left(C\right)$$
2		ssintub	$$⊢U\subseteq \bigcap \left\{s\in C|U\subseteq s\right\}$$
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	sseqtrrid	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge U\subseteq X\right)\to U\subseteq F\left(U\right)$$