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 JTopneiJ=x𝒫Xv𝒫X|gJxggv

Proof

Step Hyp Ref Expression
1 neifval.1 X=J
2 1 topopn JTopXJ
3 pwexg XJ𝒫XV
4 mptexg 𝒫XVx𝒫Xv𝒫X|gJxggvV
5 2 3 4 3syl JTopx𝒫Xv𝒫X|gJxggvV
6 unieq j=Jj=J
7 6 1 eqtr4di j=Jj=X
8 7 pweqd j=J𝒫j=𝒫X
9 rexeq j=JgjxggvgJxggv
10 8 9 rabeqbidv j=Jv𝒫j|gjxggv=v𝒫X|gJxggv
11 8 10 mpteq12dv j=Jx𝒫jv𝒫j|gjxggv=x𝒫Xv𝒫X|gJxggv
12 df-nei nei=jTopx𝒫jv𝒫j|gjxggv
13 11 12 fvmptg JTopx𝒫Xv𝒫X|gJxggvVneiJ=x𝒫Xv𝒫X|gJxggv
14 5 13 mpdan JTopneiJ=x𝒫Xv𝒫X|gJxggv