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

Definition df-ntr 18604
Description: Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval 18620. (Contributed by NM, 10-Sep-2006.)
Assertion
Ref Expression
df-ntr
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-ntr
StepHypRef Expression
1 cnt 18601 . 2
2 vj . . 3
3 ctop 18478 . . 3
4 vx . . . 4
52cv 1368 . . . . . 6
65cuni 4086 . . . . 5
76cpw 3855 . . . 4
84cv 1368 . . . . . . 7
98cpw 3855 . . . . . 6
105, 9cin 3322 . . . . 5
1110cuni 4086 . . . 4
124, 7, 11cmpt 4345 . . 3
132, 3, 12cmpt 4345 . 2
141, 13wceq 1369 1
Colors of variables: wff setvar class
This definition is referenced by:  ntrfval  18608
  Copyright terms: Public domain W3C validator