gneispaceel2

Description: Every neighborhood of a point in a generic neighborhood space contains 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	gneispaceel2	$⊢ (F \in A \land P \in dom F \land N \in F (P)) \to P \in N$

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	gneispaceel	$⊢ F \in A \to \forall p \in dom F \forall n \in F (p) p \in n$
3		fveq2	$⊢ p = P \to F (p) = F (P)$
4		eleq1	$⊢ p = P \to (p \in n \leftrightarrow P \in n)$
5	3 4	raleqbidv	$⊢ p = P \to (\forall n \in F (p) p \in n \leftrightarrow \forall n \in F (P) P \in n)$
6	5	rspccv	$⊢ \forall p \in dom F \forall n \in F (p) p \in n \to (P \in dom F \to \forall n \in F (P) P \in n)$
7	2 6	syl	$⊢ F \in A \to (P \in dom F \to \forall n \in F (P) P \in n)$
8		eleq2	$⊢ n = N \to (P \in n \leftrightarrow P \in N)$
9	8	rspccv	$⊢ \forall n \in F (P) P \in n \to (N \in F (P) \to P \in N)$
10	7 9	syl6	$⊢ F \in A \to (P \in dom F \to (N \in F (P) \to P \in N))$
11	10	3imp	$⊢ (F \in A \land P \in dom F \land N \in F (P)) \to P \in N$

Metamath Proof Explorer