gneispaceel

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	gneispaceel	$⊢ F \in A \to \forall p \in dom F \forall n \in F (p) 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	gneispace2	$⊢ F \in A \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	2	ibi	$⊢ F \in A \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))))$
4		simpl	$⊢ (p \in n \land \forall s \in 𝒫 dom F (n \subseteq s \to s \in F (p))) \to p \in n$
5	4	2ralimi	$⊢ \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))) \to \forall p \in dom F \forall n \in F (p) p \in n$
6	3 5	simpl2im	$⊢ F \in A \to \forall p \in dom F \forall n \in F (p) p \in n$

Metamath Proof Explorer