Description: Value of the neighborhood function on the subsets of the base set of a topology. (Contributed by NM, 11-Feb-2007) (Revised by Mario Carneiro, 11-Nov-2013)
Ref | Expression | ||
---|---|---|---|
Hypothesis | neifval.1 | |
|
Assertion | neifval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neifval.1 | |
|
2 | 1 | topopn | |
3 | pwexg | |
|
4 | mptexg | |
|
5 | 2 3 4 | 3syl | |
6 | unieq | |
|
7 | 6 1 | eqtr4di | |
8 | 7 | pweqd | |
9 | rexeq | |
|
10 | 8 9 | rabeqbidv | |
11 | 8 10 | mpteq12dv | |
12 | df-nei | |
|
13 | 11 12 | fvmptg | |
14 | 5 13 | mpdan | |