Metamath Proof Explorer

Theorem gneispacern2

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 ∖ \{\emptyset\}) ∖ \{\emptyset\} \land \forall p \in dom f \forall n \in f (p) (p \in n \land \forall s \in 𝒫 dom f (n \subseteq s \to s \in f (p))))\}$
	Assertion	gneispacern2	$⊢ F \in A \to ran F \subseteq 𝒫 𝒫 dom F$

Proof

Step	Hyp	Ref	Expression
1		gneispace.a	$⊢ A = \{f \| (f : dom f ⟶ 𝒫 (𝒫 dom f ∖ \{\emptyset\}) ∖ \{\emptyset\} \land \forall p \in dom f \forall n \in f (p) (p \in n \land \forall s \in 𝒫 dom f (n \subseteq s \to s \in f (p))))\}$
2		elex	$⊢ F \in A \to F \in V$
3	1	gneispace	$⊢ F \in V \to (F \in A \leftrightarrow (Fun F \land ran F \subseteq 𝒫 𝒫 dom F \land \forall p \in dom F (F (p) \neq \emptyset \land \forall n \in F (p) (p \in n \land \forall s \in 𝒫 dom F (n \subseteq s \to s \in F (p))))))$
4	2 3	syl	$⊢ F \in A \to (F \in A \leftrightarrow (Fun F \land ran F \subseteq 𝒫 𝒫 dom F \land \forall p \in dom F (F (p) \neq \emptyset \land \forall n \in F (p) (p \in n \land \forall s \in 𝒫 dom F (n \subseteq s \to s \in F (p))))))$
5	4	ibi	$⊢ F \in A \to (Fun F \land ran F \subseteq 𝒫 𝒫 dom F \land \forall p \in dom F (F (p) \neq \emptyset \land \forall n \in F (p) (p \in n \land \forall s \in 𝒫 dom F (n \subseteq s \to s \in F (p)))))$
6	5	simp2d	$⊢ F \in A \to ran F \subseteq 𝒫 𝒫 dom F$