Definition df-cld

Description: Define a function on topologies whose value is the set of closed sets of the topology. (Contributed by NM, 2-Oct-2006)

	Ref	Expression
Assertion	df-cld	|- Clsd = ( j e. Top |-> { x e. ~P U. j | ( U. j \ x ) e. j } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccld	|- Clsd
1		vj	|- j
2		ctop	|- Top
3		vx	|- x
4	1	cv	|- j
5	4	cuni	|- U. j
6	5	cpw	|- ~P U. j
7	3	cv	|- x
8	5 7	cdif	|- ( U. j \ x )
9	8 4	wcel	|- ( U. j \ x ) e. j
10	9 3 6	crab	|- { x e. ~P U. j | ( U. j \ x ) e. j }
11	1 2 10	cmpt	|- ( j e. Top |-> { x e. ~P U. j | ( U. j \ x ) e. j } )
12	0 11	wceq	|- Clsd = ( j e. Top |-> { x e. ~P U. j | ( U. j \ x ) e. j } )