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	⊢ 𝑋 = ∪ 𝐽
Assertion	gneispa	⊢ ( 𝐽 ∈ Top → ∀ 𝑝 ∈ 𝑋 ( ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) 𝑝 ∈ 𝑛 ) )

Proof

Step	Hyp	Ref	Expression
1		gneispace.x	⊢ 𝑋 = ∪ 𝐽
2		snssi	⊢ ( 𝑝 ∈ 𝑋 → { 𝑝 } ⊆ 𝑋 )
3	1	tpnei	⊢ ( 𝐽 ∈ Top → ( { 𝑝 } ⊆ 𝑋 ↔ 𝑋 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ) )
4	2 3	imbitrid	⊢ ( 𝐽 ∈ Top → ( 𝑝 ∈ 𝑋 → 𝑋 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ) )
5	4	imp	⊢ ( ( 𝐽 ∈ Top ∧ 𝑝 ∈ 𝑋 ) → 𝑋 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) )
6	5	ne0d	⊢ ( ( 𝐽 ∈ Top ∧ 𝑝 ∈ 𝑋 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ≠ ∅ )
7		elnei	⊢ ( ( 𝐽 ∈ Top ∧ 𝑝 ∈ 𝑋 ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ) → 𝑝 ∈ 𝑛 )
8	7	3expia	⊢ ( ( 𝐽 ∈ Top ∧ 𝑝 ∈ 𝑋 ) → ( 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) → 𝑝 ∈ 𝑛 ) )
9	8	ralrimiv	⊢ ( ( 𝐽 ∈ Top ∧ 𝑝 ∈ 𝑋 ) → ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) 𝑝 ∈ 𝑛 )
10	6 9	jca	⊢ ( ( 𝐽 ∈ Top ∧ 𝑝 ∈ 𝑋 ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) 𝑝 ∈ 𝑛 ) )
11	10	ralrimiva	⊢ ( 𝐽 ∈ Top → ∀ 𝑝 ∈ 𝑋 ( ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) 𝑝 ∈ 𝑛 ) )