Definition df-ntr 7664

Description: Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval 7676.

Assertion

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

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

Detailed syntax breakdown of Definition df-ntr

Step	Hyp	Ref	Expression
1		cnt 7661	. 2 class int
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	15, 9	wss 2047	. . . . . . . . . 10 wff v (_ x
17	16, 14, 3	crab 1648	. . . . . . . . 9 class {v e. z | v (_ x}
18	17	cuni 2503	. . . . . . . 8 class U.{v e. z | v (_ x}
19	13, 18	wceq 956	. . . . . . 7 wff y = U.{v e. z | v (_ x}
20	11, 19	wa 223	. . . . . 6 wff (x (_ U.z /\ y = U.{v e. z | v (_ x})
21	20, 8, 12	copab 2666	. . . . 5 class {<.x, y>. | (x (_ U.z /\ y = U.{v e. z | v (_ x})}
22	7, 21	wceq 956	. . . 4 wff w = {<.x, y>. | (x (_ U.z /\ y = U.{v e. z | v (_ x})}
23	5, 22	wa 223	. . 3 wff (z e. Top /\ w = {<.x, y>. | (x (_ U.z /\ y = U.{v e. z | v (_ x})})
24	23, 2, 6	copab 2666	. 2 class {<.z, w>. | (z e. Top /\ w = {<.x, y>. | (x (_ U.z /\ y = U.{v e. z | v (_ x})})}
25	1, 24	wceq 956	1 wff int = {<.z, w>. | (z e. Top /\ w = {<.x, y>. | (x (_ U.z /\ y = U.{v e. z | v (_ x})})}

This definition is referenced by:  ntrfval 7667

Copyright terms: Public domain