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 ∖ ∅ ∖ ∅ ∧ ∀ p ∈ dom ⁡ f ∀ n ∈ f ⁡ p p ∈ n ∧ ∀ s ∈ 𝒫 dom ⁡ f n ⊆ s → s ∈ f ⁡ p
Assertion gneispacess ⊢ F ∈ A → ∀ p ∈ dom ⁡ F ∀ n ∈ F ⁡ p ∀ s ∈ 𝒫 dom ⁡ F n ⊆ s → s ∈ F ⁡ p

Proof

Step Hyp Ref Expression
1 gneispace.a ⊢ A = f | f : dom ⁡ f ⟶ 𝒫 𝒫 dom ⁡ f ∖ ∅ ∖ ∅ ∧ ∀ p ∈ dom ⁡ f ∀ n ∈ f ⁡ p p ∈ n ∧ ∀ s ∈ 𝒫 dom ⁡ f n ⊆ s → s ∈ f ⁡ p
2 1 gneispace2 ⊢ F ∈ A → F ∈ A ↔ F : dom ⁡ F ⟶ 𝒫 𝒫 dom ⁡ F ∖ ∅ ∖ ∅ ∧ ∀ p ∈ dom ⁡ F ∀ n ∈ F ⁡ p p ∈ n ∧ ∀ s ∈ 𝒫 dom ⁡ F n ⊆ s → s ∈ F ⁡ p
3 2 ibi ⊢ F ∈ A → F : dom ⁡ F ⟶ 𝒫 𝒫 dom ⁡ F ∖ ∅ ∖ ∅ ∧ ∀ p ∈ dom ⁡ F ∀ n ∈ F ⁡ p p ∈ n ∧ ∀ s ∈ 𝒫 dom ⁡ F n ⊆ s → s ∈ F ⁡ p
4 simpr ⊢ p ∈ n ∧ ∀ s ∈ 𝒫 dom ⁡ F n ⊆ s → s ∈ F ⁡ p → ∀ s ∈ 𝒫 dom ⁡ F n ⊆ s → s ∈ F ⁡ p
5 4 2ralimi ⊢ ∀ p ∈ dom ⁡ F ∀ n ∈ F ⁡ p p ∈ n ∧ ∀ s ∈ 𝒫 dom ⁡ F n ⊆ s → s ∈ F ⁡ p → ∀ p ∈ dom ⁡ F ∀ n ∈ F ⁡ p ∀ s ∈ 𝒫 dom ⁡ F n ⊆ s → s ∈ F ⁡ p
6 3 5 simpl2im ⊢ F ∈ A → ∀ p ∈ dom ⁡ F ∀ n ∈ F ⁡ p ∀ s ∈ 𝒫 dom ⁡ F n ⊆ s → s ∈ F ⁡ p