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 = U. J
Assertion	gneispa	|- ( J e. Top -> A. p e. X ( ( ( nei ` J ) ` { p } ) =/= (/) /\ A. n e. ( ( nei ` J ) ` { p } ) p e. n ) )

Proof

Step	Hyp	Ref	Expression
1		gneispace.x	|- X = U. J
2		snssi	|- ( p e. X -> { p } C_ X )
3	1	tpnei	|- ( J e. Top -> ( { p } C_ X <-> X e. ( ( nei ` J ) ` { p } ) ) )
4	2 3	syl5ib	|- ( J e. Top -> ( p e. X -> X e. ( ( nei ` J ) ` { p } ) ) )
5	4	imp	|- ( ( J e. Top /\ p e. X ) -> X e. ( ( nei ` J ) ` { p } ) )
6	5	ne0d	|- ( ( J e. Top /\ p e. X ) -> ( ( nei ` J ) ` { p } ) =/= (/) )
7		elnei	|- ( ( J e. Top /\ p e. X /\ n e. ( ( nei ` J ) ` { p } ) ) -> p e. n )
8	7	3expia	|- ( ( J e. Top /\ p e. X ) -> ( n e. ( ( nei ` J ) ` { p } ) -> p e. n ) )
9	8	ralrimiv	|- ( ( J e. Top /\ p e. X ) -> A. n e. ( ( nei ` J ) ` { p } ) p e. n )
10	6 9	jca	|- ( ( J e. Top /\ p e. X ) -> ( ( ( nei ` J ) ` { p } ) =/= (/) /\ A. n e. ( ( nei ` J ) ` { p } ) p e. n ) )
11	10	ralrimiva	|- ( J e. Top -> A. p e. X ( ( ( nei ` J ) ` { p } ) =/= (/) /\ A. n e. ( ( nei ` J ) ` { p } ) p e. n ) )