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	$⊢ nei = (j \in Top ⟼ (x \in 𝒫 ⋃ j ⟼ \{y \in 𝒫 ⋃ j \| \exists g \in j (x \subseteq g \land g \subseteq y)\}))$

Step	Hyp	Ref	Expression
0		cnei	$class nei$
1		vj	$setvar j$
2		ctop	$class Top$
3		vx	$setvar x$
4	1	cv	$setvar j$
5	4	cuni	$class ⋃ j$
6	5	cpw	$class 𝒫 ⋃ 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 (x \subseteq g \land g \subseteq y)$
15	14 8 4	wrex	$wff \exists g \in j (x \subseteq g \land g \subseteq y)$
16	15 7 6	crab	$class \{y \in 𝒫 ⋃ j \| \exists g \in j (x \subseteq g \land g \subseteq y)\}$
17	3 6 16	cmpt	$class (x \in 𝒫 ⋃ j ⟼ \{y \in 𝒫 ⋃ j \| \exists g \in j (x \subseteq g \land g \subseteq y)\})$
18	1 2 17	cmpt	$class (j \in Top ⟼ (x \in 𝒫 ⋃ j ⟼ \{y \in 𝒫 ⋃ j \| \exists g \in j (x \subseteq g \land g \subseteq y)\}))$
19	0 18	wceq	$wff nei = (j \in Top ⟼ (x \in 𝒫 ⋃ j ⟼ \{y \in 𝒫 ⋃ j \| \exists g \in j (x \subseteq g \land g \subseteq y)\}))$

Metamath Proof Explorer