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\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	$$setvarj$$
2		ctop	$$class\mathrm{Top}$$
3		vx	$$setvarx$$
4	1	cv	$$setvarj$$
5	4	cuni	$$class\bigcup j$$
6	5	cpw	$$class𝒫\bigcup j$$
7		vy	$$setvary$$
8		vg	$$setvarg$$
9	3	cv	$$setvarx$$
10	8	cv	$$setvarg$$
11	9 10	wss	$$wffx\subseteq g$$
12	7	cv	$$setvary$$
13	10 12	wss	$$wffg\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\left(x\subseteq g\wedge g\subseteq y\right)$$
16	15 7 6	crab	$$class\left\{y\in 𝒫\bigcup j|\exists g\in j\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\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\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\left(x\subseteq g\wedge g\subseteq y\right)\right\}\right)\right)$$