Definition df-nei 22594

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

Assertion

Ref	Expression
df-nei	⊢ nei = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ {𝑦 ∈ 𝒫 ∪ 𝑗 ∣ ∃𝑔 ∈ 𝑗 (𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦)}))

Distinct variable group:   𝑔,𝑗,𝑥,𝑦

Detailed syntax breakdown of Definition df-nei

Step	Hyp	Ref	Expression
1		cnei 22593	. 2 class nei
2		vj	. . 3 setvar 𝑗
3		ctop 22387	. . 3 class Top
4		vx	. . . 4 setvar 𝑥
5	2	cv 1541	. . . . . 6 class 𝑗
6	5	cuni 4908	. . . . 5 class ∪ 𝑗
7	6	cpw 4602	. . . 4 class 𝒫 ∪ 𝑗
8	4	cv 1541	. . . . . . . 8 class 𝑥
9		vg	. . . . . . . . 9 setvar 𝑔
10	9	cv 1541	. . . . . . . 8 class 𝑔
11	8, 10	wss 3948	. . . . . . 7 wff 𝑥 ⊆ 𝑔
12		vy	. . . . . . . . 9 setvar 𝑦
13	12	cv 1541	. . . . . . . 8 class 𝑦
14	10, 13	wss 3948	. . . . . . 7 wff 𝑔 ⊆ 𝑦
15	11, 14	wa 397	. . . . . 6 wff (𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦)
16	15, 9, 5	wrex 3071	. . . . 5 wff ∃𝑔 ∈ 𝑗 (𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦)
17	16, 12, 7	crab 3433	. . . 4 class {𝑦 ∈ 𝒫 ∪ 𝑗 ∣ ∃𝑔 ∈ 𝑗 (𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦)}
18	4, 7, 17	cmpt 5231	. . 3 class (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ {𝑦 ∈ 𝒫 ∪ 𝑗 ∣ ∃𝑔 ∈ 𝑗 (𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦)})
19	2, 3, 18	cmpt 5231	. 2 class (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ {𝑦 ∈ 𝒫 ∪ 𝑗 ∣ ∃𝑔 ∈ 𝑗 (𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦)}))
20	1, 19	wceq 1542	1 wff nei = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ {𝑦 ∈ 𝒫 ∪ 𝑗 ∣ ∃𝑔 ∈ 𝑗 (𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦)}))

This definition is referenced by:  neifval  22595  neircl  47491