This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑋 ) ∧ 𝑈 ∈ 𝑋 ) → ( 𝐹 ‘ { 𝑈 } ) ∈ 𝐶 )