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 ) )