Metamath Proof Explorer

Theorem gneispace2

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	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)))))$

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		id	$⊢ f = F \to f = F$
3		dmeq	$⊢ f = F \to dom f = dom F$
4	3	pweqd	$⊢ f = F \to 𝒫 dom f = 𝒫 dom F$
5	4	difeq1d	$⊢ f = F \to 𝒫 dom f ∖ \{\emptyset\} = 𝒫 dom F ∖ \{\emptyset\}$
6	5	pweqd	$⊢ f = F \to 𝒫 (𝒫 dom f ∖ \{\emptyset\}) = 𝒫 (𝒫 dom F ∖ \{\emptyset\})$
7	6	difeq1d	$⊢ f = F \to 𝒫 (𝒫 dom f ∖ \{\emptyset\}) ∖ \{\emptyset\} = 𝒫 (𝒫 dom F ∖ \{\emptyset\}) ∖ \{\emptyset\}$
8	2 3 7	feq123d	$⊢ f = F \to (f : dom f ⟶ 𝒫 (𝒫 dom f ∖ \{\emptyset\}) ∖ \{\emptyset\} \leftrightarrow F : dom F ⟶ 𝒫 (𝒫 dom F ∖ \{\emptyset\}) ∖ \{\emptyset\})$
9		fveq1	$⊢ f = F \to f (p) = F (p)$
10	9	eleq2d	$⊢ f = F \to (s \in f (p) \leftrightarrow s \in F (p))$
11	10	imbi2d	$⊢ f = F \to ((n \subseteq s \to s \in f (p)) \leftrightarrow (n \subseteq s \to s \in F (p)))$
12	4 11	raleqbidv	$⊢ f = F \to (\forall s \in 𝒫 dom f (n \subseteq s \to s \in f (p)) \leftrightarrow \forall s \in 𝒫 dom F (n \subseteq s \to s \in F (p)))$
13	12	anbi2d	$⊢ f = F \to ((p \in n \land \forall s \in 𝒫 dom f (n \subseteq s \to s \in f (p))) \leftrightarrow (p \in n \land \forall s \in 𝒫 dom F (n \subseteq s \to s \in F (p))))$
14	9 13	raleqbidv	$⊢ f = F \to (\forall n \in f (p) (p \in n \land \forall s \in 𝒫 dom f (n \subseteq s \to s \in f (p))) \leftrightarrow \forall n \in F (p) (p \in n \land \forall s \in 𝒫 dom F (n \subseteq s \to s \in F (p))))$
15	3 14	raleqbidv	$⊢ f = F \to (\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 \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))))$
16	8 15	anbi12d	$⊢ f = F \to ((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 (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)))))$
17	16 1	elab2g	$⊢ 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)))))$