Metamath Proof Explorer


Theorem gneispacefun

Description: A generic neighborhood space is a function. (Contributed by RP, 15-Apr-2021)

Ref Expression
Hypothesis gneispace.a A=f|f:domf𝒫𝒫domfpdomfnfppns𝒫domfnssfp
Assertion gneispacefun FAFunF

Proof

Step Hyp Ref Expression
1 gneispace.a A=f|f:domf𝒫𝒫domfpdomfnfppns𝒫domfnssfp
2 1 gneispacef FAF:domF𝒫𝒫domF
3 2 ffund FAFunF