Definition df-ntr

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnt	|- int
1		vj	|- j
2		ctop	|- Top
3		vx	|- x
4	1	cv	|- j
5	4	cuni	|- U. j
6	5	cpw	|- ~P U. j
7	3	cv	|- x
8	7	cpw	|- ~P x
9	4 8	cin	|- ( j i^i ~P x )
10	9	cuni	|- U. ( j i^i ~P x )
11	3 6 10	cmpt	|- ( x e. ~P U. j |-> U. ( j i^i ~P x ) )
12	1 2 11	cmpt	|- ( j e. Top |-> ( x e. ~P U. j |-> U. ( j i^i ~P x ) ) )
13	0 12	wceq	|- int = ( j e. Top |-> ( x e. ~P U. j |-> U. ( j i^i ~P x ) ) )