Definition df-cls 7665

Description: Define a function on topologies whose value is the closure function on the subsets of the base set. See clsval 7677.

Assertion

Ref	Expression
df-cls	|- cls = {<.z, w>. | (z e. Top /\ w = {<.x, y>. | (x (_ U.z /\ y = |^|{v e. (Clsd` z) | x (_ v})})}

Distinct variable group:   w,v,x,y,z

Detailed syntax breakdown of Definition df-cls

Step	Hyp	Ref	Expression
1		ccl 7662	. 2 class cls
2		vz	. . . . . 6 set z
3	2	cv 955	. . . . 5 class z
4		ctop 7588	. . . . 5 class Top
5	3, 4	wcel 958	. . . 4 wff z e. Top
6		vw	. . . . . 6 set w
7	6	cv 955	. . . . 5 class w
8		vx	. . . . . . . . 9 set x
9	8	cv 955	. . . . . . . 8 class x
10	3	cuni 2503	. . . . . . . 8 class U.z
11	9, 10	wss 2047	. . . . . . 7 wff x (_ U.z
12		vy	. . . . . . . . 9 set y
13	12	cv 955	. . . . . . . 8 class y
14		vv	. . . . . . . . . . . 12 set v
15	14	cv 955	. . . . . . . . . . 11 class v
16	9, 15	wss 2047	. . . . . . . . . 10 wff x (_ v
17		ccld 7660	. . . . . . . . . . 11 class Clsd
18	3, 17	cfv 3182	. . . . . . . . . 10 class (Clsd` z)
19	16, 14, 18	crab 1648	. . . . . . . . 9 class {v e. (Clsd` z) | x (_ v}
20	19	cint 2533	. . . . . . . 8 class |^|{v e. (Clsd` z) | x (_ v}
21	13, 20	wceq 956	. . . . . . 7 wff y = |^|{v e. (Clsd` z) | x (_ v}
22	11, 21	wa 223	. . . . . 6 wff (x (_ U.z /\ y = |^|{v e. (Clsd` z) | x (_ v})
23	22, 8, 12	copab 2666	. . . . 5 class {<.x, y>. | (x (_ U.z /\ y = |^|{v e. (Clsd` z) | x (_ v})}
24	7, 23	wceq 956	. . . 4 wff w = {<.x, y>. | (x (_ U.z /\ y = |^|{v e. (Clsd` z) | x (_ v})}
25	5, 24	wa 223	. . 3 wff (z e. Top /\ w = {<.x, y>. | (x (_ U.z /\ y = |^|{v e. (Clsd` z) | x (_ v})})
26	25, 2, 6	copab 2666	. 2 class {<.z, w>. | (z e. Top /\ w = {<.x, y>. | (x (_ U.z /\ y = |^|{v e. (Clsd` z) | x (_ v})})}
27	1, 26	wceq 956	1 wff cls = {<.z, w>. | (z e. Top /\ w = {<.x, y>. | (x (_ U.z /\ y = |^|{v e. (Clsd` z) | x (_ v})})}

This definition is referenced by:  clsfval 7668

Copyright terms: Public domain