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	⊢ nei = ( 𝑗 ∈ Top ↦ ( 𝑥 ∈ 𝒫 ∪ 𝑗 ↦ { 𝑦 ∈ 𝒫 ∪ 𝑗 ∣ ∃ 𝑔 ∈ 𝑗 ( 𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦 ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnei	⊢ nei
1		vj	⊢ 𝑗
2		ctop	⊢ Top
3		vx	⊢ 𝑥
4	1	cv	⊢ 𝑗
5	4	cuni	⊢ ∪ 𝑗
6	5	cpw	⊢ 𝒫 ∪ 𝑗
7		vy	⊢ 𝑦
8		vg	⊢ 𝑔
9	3	cv	⊢ 𝑥
10	8	cv	⊢ 𝑔
11	9 10	wss	⊢ 𝑥 ⊆ 𝑔
12	7	cv	⊢ 𝑦
13	10 12	wss	⊢ 𝑔 ⊆ 𝑦
14	11 13	wa	⊢ ( 𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦 )
15	14 8 4	wrex	⊢ ∃ 𝑔 ∈ 𝑗 ( 𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦 )
16	15 7 6	crab	⊢ { 𝑦 ∈ 𝒫 ∪ 𝑗 ∣ ∃ 𝑔 ∈ 𝑗 ( 𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦 ) }
17	3 6 16	cmpt	⊢ ( 𝑥 ∈ 𝒫 ∪ 𝑗 ↦ { 𝑦 ∈ 𝒫 ∪ 𝑗 ∣ ∃ 𝑔 ∈ 𝑗 ( 𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦 ) } )
18	1 2 17	cmpt	⊢ ( 𝑗 ∈ Top ↦ ( 𝑥 ∈ 𝒫 ∪ 𝑗 ↦ { 𝑦 ∈ 𝒫 ∪ 𝑗 ∣ ∃ 𝑔 ∈ 𝑗 ( 𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦 ) } ) )
19	0 18	wceq	⊢ nei = ( 𝑗 ∈ Top ↦ ( 𝑥 ∈ 𝒫 ∪ 𝑗 ↦ { 𝑦 ∈ 𝒫 ∪ 𝑗 ∣ ∃ 𝑔 ∈ 𝑗 ( 𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦 ) } ) )