Metamath Proof Explorer

Theorem gneispacess

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

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	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		simpr	$⊢ (p \in n \land \forall s \in 𝒫 dom F (n \subseteq s \to s \in F (p))) \to \forall s \in 𝒫 dom F (n \subseteq s \to s \in F (p))$
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) \forall s \in 𝒫 dom F (n \subseteq s \to s \in F (p))$
6	3 5	simpl2im	$⊢ 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))$