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