Metamath Proof Explorer

Theorem gneispace3

Description: The predicate that F is a (generic) Seifert and Threlfall neighborhood space. (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	gneispace3	$⊢ F \in V \to (F \in A \leftrightarrow ((Fun F \land ran F \subseteq 𝒫 (𝒫 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)))))$

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	1	gneispace2	$⊢ F \in V \to (F \in A \leftrightarrow (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)))))$
3		df-f	$⊢ F : dom F ⟶ 𝒫 (𝒫 dom F ∖ \{\emptyset\}) ∖ \{\emptyset\} \leftrightarrow (F Fn dom F \land ran F \subseteq 𝒫 (𝒫 dom F ∖ \{\emptyset\}) ∖ \{\emptyset\})$
4		funfn	$⊢ Fun F \leftrightarrow F Fn dom F$
5	4	anbi1i	$⊢ (Fun F \land ran F \subseteq 𝒫 (𝒫 dom F ∖ \{\emptyset\}) ∖ \{\emptyset\}) \leftrightarrow (F Fn dom F \land ran F \subseteq 𝒫 (𝒫 dom F ∖ \{\emptyset\}) ∖ \{\emptyset\})$
6	3 5	bitr4i	$⊢ F : dom F ⟶ 𝒫 (𝒫 dom F ∖ \{\emptyset\}) ∖ \{\emptyset\} \leftrightarrow (Fun F \land ran F \subseteq 𝒫 (𝒫 dom F ∖ \{\emptyset\}) ∖ \{\emptyset\})$
7	6	anbi1i	$⊢ (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)))) \leftrightarrow ((Fun F \land ran F \subseteq 𝒫 (𝒫 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))))$
8	2 7	bitrdi	$⊢ F \in V \to (F \in A \leftrightarrow ((Fun F \land ran F \subseteq 𝒫 (𝒫 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)))))$