gneispacess2

Description: All supersets of a neighborhood of a point (limited to the domain of the neighborhood space) are also neighborhoods of that point. (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	gneispacess2	$⊢ ((F \in A \land P \in dom F) \land (N \in F (P) \land S \in 𝒫 dom F \land 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	gneispacess	$⊢ F \in A \to \forall p \in dom F \forall n \in F (p) \forall s \in 𝒫 dom F (n \subseteq s \to s \in F (p))$
3		fveq2	$⊢ p = P \to F (p) = F (P)$
4	3	eleq2d	$⊢ p = P \to (s \in F (p) \leftrightarrow s \in F (P))$
5	4	imbi2d	$⊢ p = P \to ((n \subseteq s \to s \in F (p)) \leftrightarrow (n \subseteq s \to s \in F (P)))$
6	5	ralbidv	$⊢ p = P \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)))$
7	3 6	raleqbidv	$⊢ p = P \to (\forall n \in F (p) \forall s \in 𝒫 dom F (n \subseteq s \to s \in F (p)) \leftrightarrow \forall n \in F (P) \forall s \in 𝒫 dom F (n \subseteq s \to s \in F (P)))$
8	7	rspccv	$⊢ \forall p \in dom F \forall n \in F (p) \forall s \in 𝒫 dom F (n \subseteq s \to s \in F (p)) \to (P \in dom F \to \forall n \in F (P) \forall s \in 𝒫 dom F (n \subseteq s \to s \in F (P)))$
9	2 8	syl	$⊢ F \in A \to (P \in dom F \to \forall n \in F (P) \forall s \in 𝒫 dom F (n \subseteq s \to s \in F (P)))$
10		sseq1	$⊢ n = N \to (n \subseteq s \leftrightarrow N \subseteq s)$
11	10	imbi1d	$⊢ n = N \to ((n \subseteq s \to s \in F (P)) \leftrightarrow (N \subseteq s \to s \in F (P)))$
12	11	ralbidv	$⊢ n = N \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	rspccv	$⊢ \forall n \in F (P) \forall s \in 𝒫 dom F (n \subseteq s \to s \in F (P)) \to (N \in F (P) \to \forall s \in 𝒫 dom F (N \subseteq s \to s \in F (P)))$
14		sseq2	$⊢ s = S \to (N \subseteq s \leftrightarrow N \subseteq S)$
15		eleq1	$⊢ s = S \to (s \in F (P) \leftrightarrow S \in F (P))$
16	14 15	imbi12d	$⊢ s = S \to ((N \subseteq s \to s \in F (P)) \leftrightarrow (N \subseteq S \to S \in F (P)))$
17	16	rspccv	$⊢ \forall s \in 𝒫 dom F (N \subseteq s \to s \in F (P)) \to (S \in 𝒫 dom F \to (N \subseteq S \to S \in F (P)))$
18	13 17	syl6	$⊢ \forall n \in F (P) \forall s \in 𝒫 dom F (n \subseteq s \to s \in F (P)) \to (N \in F (P) \to (S \in 𝒫 dom F \to (N \subseteq S \to S \in F (P))))$
19	18	3impd	$⊢ \forall n \in F (P) \forall s \in 𝒫 dom F (n \subseteq s \to s \in F (P)) \to ((N \in F (P) \land S \in 𝒫 dom F \land N \subseteq S) \to S \in F (P))$
20	9 19	syl6	$⊢ F \in A \to (P \in dom F \to ((N \in F (P) \land S \in 𝒫 dom F \land N \subseteq S) \to S \in F (P)))$
21	20	imp31	$⊢ ((F \in A \land P \in dom F) \land (N \in F (P) \land S \in 𝒫 dom F \land N \subseteq S)) \to S \in F (P)$

Metamath Proof Explorer

Theorem gneispacess2

Proof