Metamath Proof Explorer

Theorem gneispa

Description: Each point p of the neighborhood space has at least one neighborhood; each neighborhood of p contains p . Axiom A of Seifert and Threlfall. (Contributed by RP, 5-Apr-2021)

Ref Expression
Hypothesis gneispace.x ⊢ X = ⋃ J
Assertion gneispa ⊢ J ∈ Top → ∀ p ∈ X nei ⁡ J ⁡ p ≠ ∅ ∧ ∀ n ∈ nei ⁡ J ⁡ p p ∈ n

Proof

Step Hyp Ref Expression
1 gneispace.x ⊢ X = ⋃ J
2 snssi ⊢ p ∈ X → p ⊆ X
3 1 tpnei ⊢ J ∈ Top → p ⊆ X ↔ X ∈ nei ⁡ J ⁡ p
4 2 3 imbitrid ⊢ J ∈ Top → p ∈ X → X ∈ nei ⁡ J ⁡ p
5 4 imp ⊢ J ∈ Top ∧ p ∈ X → X ∈ nei ⁡ J ⁡ p
6 5 ne0d ⊢ J ∈ Top ∧ p ∈ X → nei ⁡ J ⁡ p ≠ ∅
7 elnei ⊢ J ∈ Top ∧ p ∈ X ∧ n ∈ nei ⁡ J ⁡ p → p ∈ n
8 7 3expia ⊢ J ∈ Top ∧ p ∈ X → n ∈ nei ⁡ J ⁡ p → p ∈ n
9 8 ralrimiv ⊢ J ∈ Top ∧ p ∈ X → ∀ n ∈ nei ⁡ J ⁡ p p ∈ n
10 6 9 jca ⊢ J ∈ Top ∧ p ∈ X → nei ⁡ J ⁡ p ≠ ∅ ∧ ∀ n ∈ nei ⁡ J ⁡ p p ∈ n
11 10 ralrimiva ⊢ J ∈ Top → ∀ p ∈ X nei ⁡ J ⁡ p ≠ ∅ ∧ ∀ n ∈ nei ⁡ J ⁡ p p ∈ n