Theorem gneispacef

Description: A generic neighborhood space is a function with 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	gneispacef	$$⊢F\in A\to F:\mathrm{dom}F⟶𝒫\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	gneispace2	$$⊢F\in A\to \left(F\in A\leftrightarrow \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)$$
3	2	ibi	$$⊢F\in A\to \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)$$
4	3	simpld	$$⊢F\in A\to F:\mathrm{dom}F⟶𝒫\left(𝒫\mathrm{dom}F\setminus \left\{\varnothing \right\}\right)\setminus \left\{\varnothing \right\}$$