Theorem gneispb

Description: Given a neighborhood N of P , each subset of the neighborhood space containing this neighborhood is also a neighborhood of P . Axiom B of Seifert and Threlfall. (Contributed by RP, 5-Apr-2021)

	Ref	Expression
Hypothesis	gneispace.x	|- X = U. J
Assertion	gneispb	|- ( ( J e. Top /\ P e. X /\ N e. ( ( nei ` J ) ` { P } ) ) -> A. s e. ~P X ( N C_ s -> s e. ( ( nei ` J ) ` { P } ) ) )

Proof

Step	Hyp	Ref	Expression
1		gneispace.x	|- X = U. J
2		3simpb	|- ( ( J e. Top /\ P e. X /\ N e. ( ( nei ` J ) ` { P } ) ) -> ( J e. Top /\ N e. ( ( nei ` J ) ` { P } ) ) )
3	2	ad2antrr	|- ( ( ( ( J e. Top /\ P e. X /\ N e. ( ( nei ` J ) ` { P } ) ) /\ s e. ~P X ) /\ N C_ s ) -> ( J e. Top /\ N e. ( ( nei ` J ) ` { P } ) ) )
4		simpr	|- ( ( ( ( J e. Top /\ P e. X /\ N e. ( ( nei ` J ) ` { P } ) ) /\ s e. ~P X ) /\ N C_ s ) -> N C_ s )
5		simplr	|- ( ( ( ( J e. Top /\ P e. X /\ N e. ( ( nei ` J ) ` { P } ) ) /\ s e. ~P X ) /\ N C_ s ) -> s e. ~P X )
6	5	elpwid	|- ( ( ( ( J e. Top /\ P e. X /\ N e. ( ( nei ` J ) ` { P } ) ) /\ s e. ~P X ) /\ N C_ s ) -> s C_ X )
7	1	ssnei2	|- ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` { P } ) ) /\ ( N C_ s /\ s C_ X ) ) -> s e. ( ( nei ` J ) ` { P } ) )
8	3 4 6 7	syl12anc	|- ( ( ( ( J e. Top /\ P e. X /\ N e. ( ( nei ` J ) ` { P } ) ) /\ s e. ~P X ) /\ N C_ s ) -> s e. ( ( nei ` J ) ` { P } ) )
9	8	exp31	|- ( ( J e. Top /\ P e. X /\ N e. ( ( nei ` J ) ` { P } ) ) -> ( s e. ~P X -> ( N C_ s -> s e. ( ( nei ` J ) ` { P } ) ) ) )
10	9	ralrimiv	|- ( ( J e. Top /\ P e. X /\ N e. ( ( nei ` J ) ` { P } ) ) -> A. s e. ~P X ( N C_ s -> s e. ( ( nei ` J ) ` { P } ) ) )