ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-ntr Unicode version

Definition df-ntr 12295
Description: Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval 12309. (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 12292 . 2  class  int
2 vj . . 3  setvar  j
3 ctop 12194 . . 3  class  Top
4 vx . . . 4  setvar  x
52cv 1331 . . . . . 6  class  j
65cuni 3740 . . . . 5  class  U. j
76cpw 3511 . . . 4  class  ~P U. j
84cv 1331 . . . . . . 7  class  x
98cpw 3511 . . . . . 6  class  ~P x
105, 9cin 3071 . . . . 5  class  ( j  i^i  ~P x )
1110cuni 3740 . . . 4  class  U. (
j  i^i  ~P x
)
124, 7, 11cmpt 3993 . . 3  class  ( x  e.  ~P U. j  |-> 
U. ( j  i^i 
~P x ) )
132, 3, 12cmpt 3993 . 2  class  ( j  e.  Top  |->  ( x  e.  ~P U. j  |-> 
U. ( j  i^i 
~P x ) ) )
141, 13wceq 1332 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  12299
  Copyright terms: Public domain W3C validator