Metamath Proof Explorer

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

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 gneispaceel ⊢ F ∈ A → ∀ p ∈ dom ⁡ F ∀ n ∈ F ⁡ p p ∈ n
3 fveq2 ⊢ p = P → F ⁡ p = F ⁡ P
4 eleq1 ⊢ p = P → p ∈ n ↔ P ∈ n
5 3 4 raleqbidv ⊢ p = P → ∀ n ∈ F ⁡ p p ∈ n ↔ ∀ n ∈ F ⁡ P P ∈ n
6 5 rspccv ⊢ ∀ p ∈ dom ⁡ F ∀ n ∈ F ⁡ p p ∈ n → P ∈ dom ⁡ F → ∀ n ∈ F ⁡ P P ∈ n
7 2 6 syl ⊢ F ∈ A → P ∈ dom ⁡ F → ∀ n ∈ F ⁡ P P ∈ n
8 eleq2 ⊢ n = N → P ∈ n ↔ P ∈ N
9 8 rspccv ⊢ ∀ n ∈ F ⁡ P P ∈ n → N ∈ F ⁡ P → P ∈ N
10 7 9 syl6 ⊢ F ∈ A → P ∈ dom ⁡ F → N ∈ F ⁡ P → P ∈ N
11 10 3imp ⊢ F ∈ A ∧ P ∈ dom ⁡ F ∧ N ∈ F ⁡ P → P ∈ N