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=\left\{f|\left(f:\mathrm{dom}f⟶𝒫\left(𝒫\mathrm{dom}f\setminus \left\{\varnothing \right\}\right)\setminus \left\{\varnothing \right\}\wedge \forall p\in \mathrm{dom}f\forall n\in f\left(p\right)\left(p\in n\wedge \forall s\in 𝒫\mathrm{dom}f\left(n\subseteq s\to s\in f\left(p\right)\right)\right)\right)\right\}$$
Assertion	gneispacern	$$⊢F\in A\to \mathrm{ran}F\subseteq 𝒫\left(𝒫\mathrm{dom}F\setminus \left\{\varnothing \right\}\right)\setminus \left\{\varnothing \right\}$$

Proof

Step	Hyp	Ref	Expression
1		gneispace.a	$$⊢A=\left\{f|\left(f:\mathrm{dom}f⟶𝒫\left(𝒫\mathrm{dom}f\setminus \left\{\varnothing \right\}\right)\setminus \left\{\varnothing \right\}\wedge \forall p\in \mathrm{dom}f\forall n\in f\left(p\right)\left(p\in n\wedge \forall s\in 𝒫\mathrm{dom}f\left(n\subseteq s\to s\in f\left(p\right)\right)\right)\right)\right\}$$
2	1	gneispacef	$$⊢F\in A\to F:\mathrm{dom}F⟶𝒫\left(𝒫\mathrm{dom}F\setminus \left\{\varnothing \right\}\right)\setminus \left\{\varnothing \right\}$$
3	2	frnd	$$⊢F\in A\to \mathrm{ran}F\subseteq 𝒫\left(𝒫\mathrm{dom}F\setminus \left\{\varnothing \right\}\right)\setminus \left\{\varnothing \right\}$$