Definition df-cls

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccl	|- cls
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		vy	|- y
8		ccld	|- Clsd
9	4 8	cfv	|- ( Clsd ` j )
10	3	cv	|- x
11	7	cv	|- y
12	10 11	wss	|- x C_ y
13	12 7 9	crab	|- { y e. ( Clsd ` j ) | x C_ y }
14	13	cint	|- |^| { y e. ( Clsd ` j ) | x C_ y }
15	3 6 14	cmpt	|- ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } )
16	1 2 15	cmpt	|- ( j e. Top |-> ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } ) )
17	0 16	wceq	|- cls = ( j e. Top |-> ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } ) )