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

Metamath Proof Explorer

Theorem cldval

Description: The set of closed sets of a topology. (Note that the set of open sets is just the topology itself, so we don't have a separate definition.) (Contributed by NM, 2-Oct-2006) (Revised by Mario Carneiro, 11-Nov-2013)

Ref Expression
Hypothesis cldval.1 
|- X = U. J
Assertion cldval 
|- ( J e. Top -> ( Clsd ` J ) = { x e. ~P X | ( X \ x ) e. J } )

Proof

Step Hyp Ref Expression
1 cldval.1 
 |-  X = U. J
2 1 topopn 
 |-  ( J e. Top -> X e. J )
3 pwexg 
 |-  ( X e. J -> ~P X e. _V )
4 rabexg 
 |-  ( ~P X e. _V -> { x e. ~P X | ( X \ x ) e. J } e. _V )
5 2 3 4 3syl 
 |-  ( J e. Top -> { x e. ~P X | ( X \ x ) e. J } e. _V )
6 unieq 
 |-  ( j = J -> U. j = U. J )
7 6 1 eqtr4di 
 |-  ( j = J -> U. j = X )
8 7 pweqd 
 |-  ( j = J -> ~P U. j = ~P X )
9 7 difeq1d 
 |-  ( j = J -> ( U. j \ x ) = ( X \ x ) )
10 eleq12 
 |-  ( ( ( U. j \ x ) = ( X \ x ) /\ j = J ) -> ( ( U. j \ x ) e. j <-> ( X \ x ) e. J ) )
11 9 10 mpancom 
 |-  ( j = J -> ( ( U. j \ x ) e. j <-> ( X \ x ) e. J ) )
12 8 11 rabeqbidv 
 |-  ( j = J -> { x e. ~P U. j | ( U. j \ x ) e. j } = { x e. ~P X | ( X \ x ) e. J } )
13 df-cld 
 |-  Clsd = ( j e. Top |-> { x e. ~P U. j | ( U. j \ x ) e. j } )
14 12 13 fvmptg 
 |-  ( ( J e. Top /\ { x e. ~P X | ( X \ x ) e. J } e. _V ) -> ( Clsd ` J ) = { x e. ~P X | ( X \ x ) e. J } )
15 5 14 mpdan 
 |-  ( J e. Top -> ( Clsd ` J ) = { x e. ~P X | ( X \ x ) e. J } )