This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clscld

Description: The closure of a subset of a topology's underlying set is closed. (Contributed by NM, 4-Oct-2006)

Ref Expression
Hypothesis clscld.1 
|- X = U. J
Assertion clscld 
|- ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) e. ( Clsd ` J ) )

Proof

Step Hyp Ref Expression
1 clscld.1 
 |-  X = U. J
2 1 clsval 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) = |^| { x e. ( Clsd ` J ) | S C_ x } )
3 1 topcld 
 |-  ( J e. Top -> X e. ( Clsd ` J ) )
4 3 anim1i 
 |-  ( ( J e. Top /\ S C_ X ) -> ( X e. ( Clsd ` J ) /\ S C_ X ) )
5 sseq2 
 |-  ( x = X -> ( S C_ x <-> S C_ X ) )
6 5 elrab 
 |-  ( X e. { x e. ( Clsd ` J ) | S C_ x } <-> ( X e. ( Clsd ` J ) /\ S C_ X ) )
7 4 6 sylibr 
 |-  ( ( J e. Top /\ S C_ X ) -> X e. { x e. ( Clsd ` J ) | S C_ x } )
8 7 ne0d 
 |-  ( ( J e. Top /\ S C_ X ) -> { x e. ( Clsd ` J ) | S C_ x } =/= (/) )
9 ssrab2 
 |-  { x e. ( Clsd ` J ) | S C_ x } C_ ( Clsd ` J )
10 intcld 
 |-  ( ( { x e. ( Clsd ` J ) | S C_ x } =/= (/) /\ { x e. ( Clsd ` J ) | S C_ x } C_ ( Clsd ` J ) ) -> |^| { x e. ( Clsd ` J ) | S C_ x } e. ( Clsd ` J ) )
11 8 9 10 sylancl 
 |-  ( ( J e. Top /\ S C_ X ) -> |^| { x e. ( Clsd ` J ) | S C_ x } e. ( Clsd ` J ) )
12 2 11 eqeltrd 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) e. ( Clsd ` J ) )