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 = U. J
Assertion cldmre
|- ( J e. Top -> ( Clsd ` J ) e. ( Moore ` X ) )

Proof

Step Hyp Ref Expression
1 clscld.1
 |-  X = U. J
2 1 cldss2
 |-  ( Clsd ` J ) C_ ~P X
3 2 a1i
 |-  ( J e. Top -> ( Clsd ` J ) C_ ~P X )
4 1 topcld
 |-  ( J e. Top -> X e. ( Clsd ` J ) )
5 intcld
 |-  ( ( x =/= (/) /\ x C_ ( Clsd ` J ) ) -> |^| x e. ( Clsd ` J ) )
6 5 ancoms
 |-  ( ( x C_ ( Clsd ` J ) /\ x =/= (/) ) -> |^| x e. ( Clsd ` J ) )
7 6 3adant1
 |-  ( ( J e. Top /\ x C_ ( Clsd ` J ) /\ x =/= (/) ) -> |^| x e. ( Clsd ` J ) )
8 3 4 7 ismred
 |-  ( J e. Top -> ( Clsd ` J ) e. ( Moore ` X ) )