Metamath Proof Explorer


Theorem neif

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

Ref Expression
Hypothesis neifval.1 X = J
Assertion neif J Top nei J Fn 𝒫 X

Proof

Step Hyp Ref Expression
1 neifval.1 X = J
2 1 topopn J Top X J
3 pwexg X J 𝒫 X V
4 rabexg 𝒫 X V v 𝒫 X | g J x g g v V
5 2 3 4 3syl J Top v 𝒫 X | g J x g g v V
6 5 ralrimivw J Top x 𝒫 X v 𝒫 X | g J x g g v V
7 eqid x 𝒫 X v 𝒫 X | g J x g g v = x 𝒫 X v 𝒫 X | g J x g g v
8 7 fnmpt x 𝒫 X v 𝒫 X | g J x g g v V x 𝒫 X v 𝒫 X | g J x g g v Fn 𝒫 X
9 6 8 syl J Top x 𝒫 X v 𝒫 X | g J x g g v Fn 𝒫 X
10 1 neifval J Top nei J = x 𝒫 X v 𝒫 X | g J x g g v
11 10 fneq1d J Top nei J Fn 𝒫 X x 𝒫 X v 𝒫 X | g J x g g v Fn 𝒫 X
12 9 11 mpbird J Top nei J Fn 𝒫 X