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