Metamath Proof Explorer

Theorem gneispacef2

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 = \{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	gneispacef2	$⊢ F \in A \to F : dom F ⟶ 𝒫 𝒫 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		simp1	$⊢ (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))))) \to Fun F$
7	6	funfnd	$⊢ (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))))) \to F Fn dom F$
8		simp2	$⊢ (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))))) \to ran F \subseteq 𝒫 𝒫 dom F$
9		df-f	$⊢ F : dom F ⟶ 𝒫 𝒫 dom F \leftrightarrow (F Fn dom F \land ran F \subseteq 𝒫 𝒫 dom F)$
10	7 8 9	sylanbrc	$⊢ (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))))) \to F : dom F ⟶ 𝒫 𝒫 dom F$
11	5 10	syl	$⊢ F \in A \to F : dom F ⟶ 𝒫 𝒫 dom F$