Definition df-cls 12255

Description: Define a function on topologies whose value is the closure function on the subsets of the base set. See clsval 12269. (Contributed by NM, 3-Oct-2006.)

Assertion

Ref	Expression
df-cls	|- cls = ( j e. Top |-> ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } ) )

Distinct variable group:   x, j, y

Detailed syntax breakdown of Definition df-cls

Step	Hyp	Ref	Expression
1		ccl 12252	. 2 class cls
2		vj	. . 3 setvar j
3		ctop 12153	. . 3 class Top
4		vx	. . . 4 setvar x
5	2	cv 1330	. . . . . 6 class j
6	5	cuni 3731	. . . . 5 class U. j
7	6	cpw 3505	. . . 4 class ~P U. j
8	4	cv 1330	. . . . . . 7 class x
9		vy	. . . . . . . 8 setvar y
10	9	cv 1330	. . . . . . 7 class y
11	8, 10	wss 3066	. . . . . 6 wff x C_ y
12		ccld 12250	. . . . . . 7 class Clsd
13	5, 12	cfv 5118	. . . . . 6 class ( Clsd ` j )
14	11, 9, 13	crab 2418	. . . . 5 class { y e. ( Clsd ` j ) | x C_ y }
15	14	cint 3766	. . . 4 class |^| { y e. ( Clsd ` j ) | x C_ y }
16	4, 7, 15	cmpt 3984	. . 3 class ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } )
17	2, 3, 16	cmpt 3984	. 2 class ( j e. Top |-> ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } ) )
18	1, 17	wceq 1331	1 wff cls = ( j e. Top |-> ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } ) )

This definition is referenced by:  clsfval  12259