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 F=mrClsC
Assertion mrcsncl CMooreXUXFUC

Proof

Step Hyp Ref Expression
1 mrcfval.f F=mrClsC
2 snssi UXUX
3 1 mrccl CMooreXUXFUC
4 2 3 sylan2 CMooreXUXFUC