MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-nei Structured version   Visualization version   GIF version

Definition df-nei 22230
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
StepHypRef Expression
1 cnei 22229 . 2 class nei
2 vj . . 3 setvar 𝑗
3 ctop 22023 . . 3 class Top
4 vx . . . 4 setvar 𝑥
52cv 1540 . . . . . 6 class 𝑗
65cuni 4844 . . . . 5 class 𝑗
76cpw 4538 . . . 4 class 𝒫 𝑗
84cv 1540 . . . . . . . 8 class 𝑥
9 vg . . . . . . . . 9 setvar 𝑔
109cv 1540 . . . . . . . 8 class 𝑔
118, 10wss 3891 . . . . . . 7 wff 𝑥𝑔
12 vy . . . . . . . . 9 setvar 𝑦
1312cv 1540 . . . . . . . 8 class 𝑦
1410, 13wss 3891 . . . . . . 7 wff 𝑔𝑦
1511, 14wa 395 . . . . . 6 wff (𝑥𝑔𝑔𝑦)
1615, 9, 5wrex 3066 . . . . 5 wff 𝑔𝑗 (𝑥𝑔𝑔𝑦)
1716, 12, 7crab 3069 . . . 4 class {𝑦 ∈ 𝒫 𝑗 ∣ ∃𝑔𝑗 (𝑥𝑔𝑔𝑦)}
184, 7, 17cmpt 5161 . . 3 class (𝑥 ∈ 𝒫 𝑗 ↦ {𝑦 ∈ 𝒫 𝑗 ∣ ∃𝑔𝑗 (𝑥𝑔𝑔𝑦)})
192, 3, 18cmpt 5161 . 2 class (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 𝑗 ↦ {𝑦 ∈ 𝒫 𝑗 ∣ ∃𝑔𝑗 (𝑥𝑔𝑔𝑦)}))
201, 19wceq 1541 1 wff nei = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 𝑗 ↦ {𝑦 ∈ 𝒫 𝑗 ∣ ∃𝑔𝑗 (𝑥𝑔𝑔𝑦)}))
Colors of variables: wff setvar class
This definition is referenced by:  neifval  22231  neircl  46150
  Copyright terms: Public domain W3C validator