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

Metamath Proof Explorer

Theorem iscld

Description: The predicate "the class S is a closed set". (Contributed by NM, 2-Oct-2006) (Revised by Mario Carneiro, 11-Nov-2013)

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

Proof

Step Hyp Ref Expression
1 iscld.1 
 |-  X = U. J
2 1 cldval 
 |-  ( J e. Top -> ( Clsd ` J ) = { x e. ~P X | ( X \ x ) e. J } )
3 2 eleq2d 
 |-  ( J e. Top -> ( S e. ( Clsd ` J ) <-> S e. { x e. ~P X | ( X \ x ) e. J } ) )
4 difeq2 
 |-  ( x = S -> ( X \ x ) = ( X \ S ) )
5 4 eleq1d 
 |-  ( x = S -> ( ( X \ x ) e. J <-> ( X \ S ) e. J ) )
6 5 elrab 
 |-  ( S e. { x e. ~P X | ( X \ x ) e. J } <-> ( S e. ~P X /\ ( X \ S ) e. J ) )
7 3 6 bitrdi 
 |-  ( J e. Top -> ( S e. ( Clsd ` J ) <-> ( S e. ~P X /\ ( X \ S ) e. J ) ) )
8 1 topopn 
 |-  ( J e. Top -> X e. J )
9 elpw2g 
 |-  ( X e. J -> ( S e. ~P X <-> S C_ X ) )
10 8 9 syl 
 |-  ( J e. Top -> ( S e. ~P X <-> S C_ X ) )
11 10 anbi1d 
 |-  ( J e. Top -> ( ( S e. ~P X /\ ( X \ S ) e. J ) <-> ( S C_ X /\ ( X \ S ) e. J ) ) )
12 7 11 bitrd 
 |-  ( J e. Top -> ( S e. ( Clsd ` J ) <-> ( S C_ X /\ ( X \ S ) e. J ) ) )