Definition df-cld 20823

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

Assertion

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

Distinct variable group:   x, j

Detailed syntax breakdown of Definition df-cld

Step	Hyp	Ref	Expression
1		ccld 20820	. 2 class Clsd
2		vj	. . 3 setvar j
3		ctop 20698	. . 3 class Top
4	2	cv 1482	. . . . . . 7 class j
5	4	cuni 4436	. . . . . 6 class U. j
6		vx	. . . . . . 7 setvar x
7	6	cv 1482	. . . . . 6 class x
8	5, 7	cdif 3571	. . . . 5 class ( U. j \ x )
9	8, 4	wcel 1990	. . . 4 wff ( U. j \ x ) e. j
10	5	cpw 4158	. . . 4 class ~P U. j
11	9, 6, 10	crab 2916	. . 3 class { x e. ~P U. j | ( U. j \ x ) e. j }
12	2, 3, 11	cmpt 4729	. 2 class ( j e. Top |-> { x e. ~P U. j | ( U. j \ x ) e. j } )
13	1, 12	wceq 1483	1 wff Clsd = ( j e. Top |-> { x e. ~P U. j | ( U. j \ x ) e. j } )

This definition is referenced by:  fncld  20826  cldval  20827