Metamath Proof Explorer


Theorem neifval

Description: Value of the neighborhood function on the subsets of the base set of a topology. (Contributed by NM, 11-Feb-2007) (Revised by Mario Carneiro, 11-Nov-2013)

Ref Expression
Hypothesis neifval.1 X = J
Assertion neifval J Top nei J = x 𝒫 X v 𝒫 X | g J x g g v

Proof

Step Hyp Ref Expression
1 neifval.1 X = J
2 1 topopn J Top X J
3 pwexg X J 𝒫 X V
4 mptexg 𝒫 X V x 𝒫 X v 𝒫 X | g J x g g v V
5 2 3 4 3syl J Top x 𝒫 X v 𝒫 X | g J x g g v V
6 unieq j = J j = J
7 6 1 eqtr4di j = J j = X
8 7 pweqd j = J 𝒫 j = 𝒫 X
9 rexeq j = J g j x g g v g J x g g v
10 8 9 rabeqbidv j = J v 𝒫 j | g j x g g v = v 𝒫 X | g J x g g v
11 8 10 mpteq12dv j = J x 𝒫 j v 𝒫 j | g j x g g v = x 𝒫 X v 𝒫 X | g J x g g v
12 df-nei nei = j Top x 𝒫 j v 𝒫 j | g j x g g v
13 11 12 fvmptg J Top x 𝒫 X v 𝒫 X | g J x g g v V nei J = x 𝒫 X v 𝒫 X | g J x g g v
14 5 13 mpdan J Top nei J = x 𝒫 X v 𝒫 X | g J x g g v