Definition df-cls 8941

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

Assertion

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

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

Detailed syntax breakdown of Definition df-cls

Step	Hyp	Ref	Expression
1		ccl 8938	. 2 class cls
2		vz	. . . . . 6 set z
3	2	cv 1297	. . . . 5 class z
4		ctop 8857	. . . . 5 class Top
5	3, 4	wcel 1300	. . . 4 wff z e. Top
6		vw	. . . . . 6 set w
7	6	cv 1297	. . . . 5 class w
8		vx	. . . . . . . . 9 set x
9	8	cv 1297	. . . . . . . 8 class x
10	3	cuni 3177	. . . . . . . 8 class U.z
11	9, 10	wss 2593	. . . . . . 7 wff x C_ U.z
12		vy	. . . . . . . . 9 set y
13	12	cv 1297	. . . . . . . 8 class y
14		vv	. . . . . . . . . . . 12 set v
15	14	cv 1297	. . . . . . . . . . 11 class v
16	9, 15	wss 2593	. . . . . . . . . 10 wff x C_ v
17		ccld 8936	. . . . . . . . . . 11 class Clsd
18	3, 17	cfv 3998	. . . . . . . . . 10 class (Clsd` z)
19	16, 14, 18	crab 2108	. . . . . . . . 9 class {v e. (Clsd` z) | x C_ v}
20	19	cint 3214	. . . . . . . 8 class |^|{v e. (Clsd` z) | x C_ v}
21	13, 20	wceq 1298	. . . . . . 7 wff y = |^|{v e. (Clsd` z) | x C_ v}
22	11, 21	wa 240	. . . . . 6 wff (x C_ U.z /\ y = |^|{v e. (Clsd` z) | x C_ v})
23	22, 8, 12	copab 3395	. . . . 5 class {<.x, y>. | (x C_ U.z /\ y = |^|{v e. (Clsd` z) | x C_ v})}
24	7, 23	wceq 1298	. . . 4 wff w = {<.x, y>. | (x C_ U.z /\ y = |^|{v e. (Clsd` z) | x C_ v})}
25	5, 24	wa 240	. . 3 wff (z e. Top /\ w = {<.x, y>. | (x C_ U.z /\ y = |^|{v e. (Clsd` z) | x C_ v})})
26	25, 2, 6	copab 3395	. 2 class {<.z, w>. | (z e. Top /\ w = {<.x, y>. | (x C_ U.z /\ y = |^|{v e. (Clsd` z) | x C_ v})})}
27	1, 26	wceq 1298	1 wff cls = {<.z, w>. | (z e. Top /\ w = {<.x, y>. | (x C_ U.z /\ y = |^|{v e. (Clsd` z) | x C_ v})})}

This definition is referenced by:  clsfval 8944

Copyright terms: Public domain