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

Definition df-nei 17162
 Description: Define a function on topologies whose value is a map from a subset to its neighborhoods. (Contributed by NM, 11-Feb-2007.)
Assertion
Ref Expression
df-nei
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-nei
StepHypRef Expression
1 cnei 17161 . 2
2 vj . . 3
3 ctop 16958 . . 3
4 vx . . . 4
52cv 1651 . . . . . 6
65cuni 4015 . . . . 5
76cpw 3799 . . . 4
84cv 1651 . . . . . . . 8
9 vg . . . . . . . . 9
109cv 1651 . . . . . . . 8
118, 10wss 3320 . . . . . . 7
12 vy . . . . . . . . 9
1312cv 1651 . . . . . . . 8
1410, 13wss 3320 . . . . . . 7
1511, 14wa 359 . . . . . 6
1615, 9, 5wrex 2706 . . . . 5
1716, 12, 7crab 2709 . . . 4
184, 7, 17cmpt 4266 . . 3
192, 3, 18cmpt 4266 . 2
201, 19wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  neifval  17163
 Copyright terms: Public domain W3C validator