# Metamath Proof Explorer

## Definition df-nei

Description: Define a function on topologies whose value is a map from a subset to its neighborhoods. (Contributed by NM, 11-Feb-2007)

Ref Expression
Assertion df-nei ${⊢}\mathrm{nei}=\left({j}\in \mathrm{Top}⟼\left({x}\in 𝒫\bigcup {j}⟼\left\{{y}\in 𝒫\bigcup {j}|\exists {g}\in {j}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {g}\wedge {g}\subseteq {y}\right)\right\}\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cnei ${class}\mathrm{nei}$
1 vj ${setvar}{j}$
2 ctop ${class}\mathrm{Top}$
3 vx ${setvar}{x}$
4 1 cv ${setvar}{j}$
5 4 cuni ${class}\bigcup {j}$
6 5 cpw ${class}𝒫\bigcup {j}$
7 vy ${setvar}{y}$
8 vg ${setvar}{g}$
9 3 cv ${setvar}{x}$
10 8 cv ${setvar}{g}$
11 9 10 wss ${wff}{x}\subseteq {g}$
12 7 cv ${setvar}{y}$
13 10 12 wss ${wff}{g}\subseteq {y}$
14 11 13 wa ${wff}\left({x}\subseteq {g}\wedge {g}\subseteq {y}\right)$
15 14 8 4 wrex ${wff}\exists {g}\in {j}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {g}\wedge {g}\subseteq {y}\right)$
16 15 7 6 crab ${class}\left\{{y}\in 𝒫\bigcup {j}|\exists {g}\in {j}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {g}\wedge {g}\subseteq {y}\right)\right\}$
17 3 6 16 cmpt ${class}\left({x}\in 𝒫\bigcup {j}⟼\left\{{y}\in 𝒫\bigcup {j}|\exists {g}\in {j}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {g}\wedge {g}\subseteq {y}\right)\right\}\right)$
18 1 2 17 cmpt ${class}\left({j}\in \mathrm{Top}⟼\left({x}\in 𝒫\bigcup {j}⟼\left\{{y}\in 𝒫\bigcup {j}|\exists {g}\in {j}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {g}\wedge {g}\subseteq {y}\right)\right\}\right)\right)$
19 0 18 wceq ${wff}\mathrm{nei}=\left({j}\in \mathrm{Top}⟼\left({x}\in 𝒫\bigcup {j}⟼\left\{{y}\in 𝒫\bigcup {j}|\exists {g}\in {j}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {g}\wedge {g}\subseteq {y}\right)\right\}\right)\right)$