gneispace0nelrn2

Description: A generic neighborhood space has a nonempty set of neighborhoods for every point in its domain. (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	gneispace0nelrn2	$⊢ (F \in A \land P \in dom F) \to F (P) \neq \emptyset$

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	gneispace0nelrn	$⊢ F \in A \to \forall p \in dom F F (p) \neq \emptyset$
3		fveq2	$⊢ p = P \to F (p) = F (P)$
4	3	neeq1d	$⊢ p = P \to (F (p) \neq \emptyset \leftrightarrow F (P) \neq \emptyset)$
5	4	rspccv	$⊢ \forall p \in dom F F (p) \neq \emptyset \to (P \in dom F \to F (P) \neq \emptyset)$
6	2 5	syl	$⊢ F \in A \to (P \in dom F \to F (P) \neq \emptyset)$
7	6	imp	$⊢ (F \in A \land P \in dom F) \to F (P) \neq \emptyset$

Metamath Proof Explorer