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 = ( mrCls ` C )
Assertion	mrcsncl	|- ( ( C e. ( Moore ` X ) /\ U e. X ) -> ( F ` { U } ) e. C )

Proof

Step	Hyp	Ref	Expression
1		mrcfval.f	|- F = ( mrCls ` C )
2		snssi	|- ( U e. X -> { U } C_ X )
3	1	mrccl	|- ( ( C e. ( Moore ` X ) /\ { U } C_ X ) -> ( F ` { U } ) e. C )
4	2 3	sylan2	|- ( ( C e. ( Moore ` X ) /\ U e. X ) -> ( F ` { U } ) e. C )