Theorem mrcsncl

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

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

Proof

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