Metamath Proof Explorer


Theorem cldmre

Description: The closed sets of a topology comprise a Moore system on the points of the topology. (Contributed by Stefan O'Rear, 31-Jan-2015)

Ref Expression
Hypothesis clscld.1 X = J
Assertion cldmre J Top Clsd J Moore X

Proof

Step Hyp Ref Expression
1 clscld.1 X = J
2 1 cldss2 Clsd J 𝒫 X
3 2 a1i J Top Clsd J 𝒫 X
4 1 topcld J Top X Clsd J
5 intcld x x Clsd J x Clsd J
6 5 ancoms x Clsd J x x Clsd J
7 6 3adant1 J Top x Clsd J x x Clsd J
8 3 4 7 ismred J Top Clsd J Moore X