Definition df-cld 9800

Description: Define a function on topologies whose value is the set of closed sets of the topology.

Assertion

Ref	Expression
df-cld	|- Clsd = {<.z, w>. | (z e. Top /\ w = {x | (x C_ U.z /\ (U.z \ x) e. z)})}

Distinct variable group:   x,w,z

Detailed syntax breakdown of Definition df-cld

Step	Hyp	Ref	Expression
1		ccld 9797	. 2 class Clsd
2		vz	. . . . . 6 set z
3	2	cv 1585	. . . . 5 class z
4		ctop 9686	. . . . 5 class Top
5	3, 4	wcel 1588	. . . 4 wff z e. Top
6		vw	. . . . . 6 set w
7	6	cv 1585	. . . . 5 class w
8		vx	. . . . . . . . 9 set x
9	8	cv 1585	. . . . . . . 8 class x
10	3	cuni 3366	. . . . . . . 8 class U.z
11	9, 10	wss 2827	. . . . . . 7 wff x C_ U.z
12	10, 9	cdif 2824	. . . . . . . 8 class (U.z \ x)
13	12, 3	wcel 1588	. . . . . . 7 wff (U.z \ x) e. z
14	11, 13	wa 337	. . . . . 6 wff (x C_ U.z /\ (U.z \ x) e. z)
15	14, 8	cab 2128	. . . . 5 class {x | (x C_ U.z /\ (U.z \ x) e. z)}
16	7, 15	wceq 1586	. . . 4 wff w = {x | (x C_ U.z /\ (U.z \ x) e. z)}
17	5, 16	wa 337	. . 3 wff (z e. Top /\ w = {x | (x C_ U.z /\ (U.z \ x) e. z)})
18	17, 2, 6	copab 3565	. 2 class {<.z, w>. | (z e. Top /\ w = {x | (x C_ U.z /\ (U.z \ x) e. z)})}
19	1, 18	wceq 1586	1 wff Clsd = {<.z, w>. | (z e. Top /\ w = {x | (x C_ U.z /\ (U.z \ x) e. z)})}

This definition is referenced by:  cldval 9803

Copyright terms: Public domain