MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ntr Structured version   Unicode version

Definition df-ntr 17089
Description: Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval 17105. (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
StepHypRef Expression
1 cnt 17086 . 2  class  int
2 vj . . 3  set  j
3 ctop 16963 . . 3  class  Top
4 vx . . . 4  set  x
52cv 1652 . . . . . 6  class  j
65cuni 4017 . . . . 5  class  U. j
76cpw 3801 . . . 4  class  ~P U. j
84cv 1652 . . . . . . 7  class  x
98cpw 3801 . . . . . 6  class  ~P x
105, 9cin 3321 . . . . 5  class  ( j  i^i  ~P x )
1110cuni 4017 . . . 4  class  U. (
j  i^i  ~P x
)
124, 7, 11cmpt 4269 . . 3  class  ( x  e.  ~P U. j  |-> 
U. ( j  i^i 
~P x ) )
132, 3, 12cmpt 4269 . 2  class  ( j  e.  Top  |->  ( x  e.  ~P U. j  |-> 
U. ( j  i^i 
~P x ) ) )
141, 13wceq 1653 1  wff  int  =  ( j  e.  Top  |->  ( x  e.  ~P U. j  |->  U. ( j  i^i 
~P x ) ) )
Colors of variables: wff set class
This definition is referenced by:  ntrfval  17093
  Copyright terms: Public domain W3C validator