Metamath Proof Explorer


Theorem gneispacern

Description: A generic neighborhood space has a range that is a subset of the powerset of the powerset of its domain. (Contributed by RP, 15-Apr-2021)

Ref Expression
Hypothesis gneispace.a A = f | f : dom f 𝒫 𝒫 dom f p dom f n f p p n s 𝒫 dom f n s s f p
Assertion gneispacern F A ran F 𝒫 𝒫 dom F

Proof

Step Hyp Ref Expression
1 gneispace.a A = f | f : dom f 𝒫 𝒫 dom f p dom f n f p p n s 𝒫 dom f n s s f p
2 1 gneispacef F A F : dom F 𝒫 𝒫 dom F
3 2 frnd F A ran F 𝒫 𝒫 dom F