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

Definition df-ntr 16757
Description: Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval 16773. (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 16754 . 2  class  int
2 vj . . 3  set  j
3 ctop 16631 . . 3  class  Top
4 vx . . . 4  set  x
52cv 1622 . . . . . 6  class  j
65cuni 3827 . . . . 5  class  U. j
76cpw 3625 . . . 4  class  ~P U. j
84cv 1622 . . . . . . 7  class  x
98cpw 3625 . . . . . 6  class  ~P x
105, 9cin 3151 . . . . 5  class  ( j  i^i  ~P x )
1110cuni 3827 . . . 4  class  U. (
j  i^i  ~P x
)
124, 7, 11cmpt 4077 . . 3  class  ( x  e.  ~P U. j  |-> 
U. ( j  i^i 
~P x ) )
132, 3, 12cmpt 4077 . 2  class  ( j  e.  Top  |->  ( x  e.  ~P U. j  |-> 
U. ( j  i^i 
~P x ) ) )
141, 13wceq 1623 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  16761
  Copyright terms: Public domain W3C validator