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	⊢ 𝐹 = ( mrCls ‘ 𝐶 )
Assertion	mrcsncl	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ∈ 𝑋 ) → ( 𝐹 ‘ { 𝑈 } ) ∈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		mrcfval.f	⊢ 𝐹 = ( mrCls ‘ 𝐶 )
2		snssi	⊢ ( 𝑈 ∈ 𝑋 → { 𝑈 } ⊆ 𝑋 )
3	1	mrccl	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ { 𝑈 } ⊆ 𝑋 ) → ( 𝐹 ‘ { 𝑈 } ) ∈ 𝐶 )
4	2 3	sylan2	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ∈ 𝑋 ) → ( 𝐹 ‘ { 𝑈 } ) ∈ 𝐶 )