Definition df-ntr 12890

Description: Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval 12904. (Contributed by NM, 10-Sep-2006.)

Assertion

Ref	Expression
df-ntr	|- int = ( j e. Top |-> ( x e. ~P U. j |-> U. ( j i^i ~P x ) ) )

Distinct variable group:   x, j

Detailed syntax breakdown of Definition df-ntr

Step	Hyp	Ref	Expression
1		cnt 12887	. 2 class int
2		vj	. . 3 setvar j
3		ctop 12789	. . 3 class Top
4		vx	. . . 4 setvar x
5	2	cv 1347	. . . . . 6 class j
6	5	cuni 3796	. . . . 5 class U. j
7	6	cpw 3566	. . . 4 class ~P U. j
8	4	cv 1347	. . . . . . 7 class x
9	8	cpw 3566	. . . . . 6 class ~P x
10	5, 9	cin 3120	. . . . 5 class ( j i^i ~P x )
11	10	cuni 3796	. . . 4 class U. ( j i^i ~P x )
12	4, 7, 11	cmpt 4050	. . 3 class ( x e. ~P U. j |-> U. ( j i^i ~P x ) )
13	2, 3, 12	cmpt 4050	. 2 class ( j e. Top |-> ( x e. ~P U. j |-> U. ( j i^i ~P x ) ) )
14	1, 13	wceq 1348	1 wff int = ( j e. Top |-> ( x e. ~P U. j |-> U. ( j i^i ~P x ) ) )

This definition is referenced by:  ntrfval  12894