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=\bigcup J$$
Assertion	gneispa	$$⊢J\in \mathrm{Top}\to \forall p\in X\left(\mathrm{nei}\left(J\right)\left(\left\{p\right\}\right)\ne \varnothing \wedge \forall n\in \mathrm{nei}\left(J\right)\left(\left\{p\right\}\right)p\in n\right)$$

Proof

Step	Hyp	Ref	Expression
1		gneispace.x	$$⊢X=\bigcup J$$
2		snssi	$$⊢p\in X\to \left\{p\right\}\subseteq X$$
3	1	tpnei	$$⊢J\in \mathrm{Top}\to \left(\left\{p\right\}\subseteq X\leftrightarrow X\in \mathrm{nei}\left(J\right)\left(\left\{p\right\}\right)\right)$$
4	2 3	imbitrid	$$⊢J\in \mathrm{Top}\to \left(p\in X\to X\in \mathrm{nei}\left(J\right)\left(\left\{p\right\}\right)\right)$$
5	4	imp	$$⊢\left(J\in \mathrm{Top}\wedge p\in X\right)\to X\in \mathrm{nei}\left(J\right)\left(\left\{p\right\}\right)$$
6	5	ne0d	$$⊢\left(J\in \mathrm{Top}\wedge p\in X\right)\to \mathrm{nei}\left(J\right)\left(\left\{p\right\}\right)\ne \varnothing$$
7		elnei	$$⊢\left(J\in \mathrm{Top}\wedge p\in X\wedge n\in \mathrm{nei}\left(J\right)\left(\left\{p\right\}\right)\right)\to p\in n$$
8	7	3expia	$$⊢\left(J\in \mathrm{Top}\wedge p\in X\right)\to \left(n\in \mathrm{nei}\left(J\right)\left(\left\{p\right\}\right)\to p\in n\right)$$
9	8	ralrimiv	$$⊢\left(J\in \mathrm{Top}\wedge p\in X\right)\to \forall n\in \mathrm{nei}\left(J\right)\left(\left\{p\right\}\right)p\in n$$
10	6 9	jca	$$⊢\left(J\in \mathrm{Top}\wedge p\in X\right)\to \left(\mathrm{nei}\left(J\right)\left(\left\{p\right\}\right)\ne \varnothing \wedge \forall n\in \mathrm{nei}\left(J\right)\left(\left\{p\right\}\right)p\in n\right)$$
11	10	ralrimiva	$$⊢J\in \mathrm{Top}\to \forall p\in X\left(\mathrm{nei}\left(J\right)\left(\left\{p\right\}\right)\ne \varnothing \wedge \forall n\in \mathrm{nei}\left(J\right)\left(\left\{p\right\}\right)p\in n\right)$$