Metamath Proof Explorer


Theorem mrcid

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

Ref Expression
Hypothesis mrcfval.f F=mrClsC
Assertion mrcid CMooreXUCFU=U

Proof

Step Hyp Ref Expression
1 mrcfval.f F=mrClsC
2 mress CMooreXUCUX
3 1 mrcval CMooreXUXFU=sC|Us
4 2 3 syldan CMooreXUCFU=sC|Us
5 intmin UCsC|Us=U
6 5 adantl CMooreXUCsC|Us=U
7 4 6 eqtrd CMooreXUCFU=U