Definition df-cld 7660

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 (_ 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 7657	. 2 class Clsd
2		vz	. . . . . 6 set z
3	2	cv 957	. . . . 5 class z
4		ctop 7590	. . . . 5 class Top
5	3, 4	wcel 960	. . . 4 wff z e. Top
6		vw	. . . . . 6 set w
7	6	cv 957	. . . . 5 class w
8		vx	. . . . . . . . 9 set x
9	8	cv 957	. . . . . . . 8 class x
10	3	cuni 2507	. . . . . . . 8 class U.z
11	9, 10	wss 2050	. . . . . . 7 wff x (_ U.z
12	10, 9	cdif 2047	. . . . . . . 8 class (U.z \ x)
13	12, 3	wcel 960	. . . . . . 7 wff (U.z \ x) e. z
14	11, 13	wa 223	. . . . . 6 wff (x (_ U.z /\ (U.z \ x) e. z)
15	14, 8	cab 1466	. . . . 5 class {x | (x (_ U.z /\ (U.z \ x) e. z)}
16	7, 15	wceq 958	. . . 4 wff w = {x | (x (_ U.z /\ (U.z \ x) e. z)}
17	5, 16	wa 223	. . 3 wff (z e. Top /\ w = {x | (x (_ U.z /\ (U.z \ x) e. z)})
18	17, 2, 6	copab 2671	. 2 class {<.z, w>. | (z e. Top /\ w = {x | (x (_ U.z /\ (U.z \ x) e. z)})}
19	1, 18	wceq 958	1 wff Clsd = {<.z, w>. | (z e. Top /\ w = {x | (x (_ U.z /\ (U.z \ x) e. z)})}

This definition is referenced by:  cldval 7663

Copyright terms: Public domain