Metamath Proof Explorer


Theorem mrcssv

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

Ref Expression
Hypothesis mrcfval.f F=mrClsC
Assertion mrcssv CMooreXFUX

Proof

Step Hyp Ref Expression
1 mrcfval.f F=mrClsC
2 fvssunirn FUranF
3 1 mrcf CMooreXF:𝒫XC
4 frn F:𝒫XCranFC
5 uniss ranFCranFC
6 3 4 5 3syl CMooreXranFC
7 mreuni CMooreXC=X
8 6 7 sseqtrd CMooreXranFX
9 2 8 sstrid CMooreXFUX