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	⊢ 𝑋 = ∪ 𝐽
Assertion	gneispb	⊢ ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) → ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑁 ⊆ 𝑠 → 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		gneispace.x	⊢ 𝑋 = ∪ 𝐽
2		3simpb	⊢ ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) → ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) )
3	2	ad2antrr	⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑁 ⊆ 𝑠 ) → ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) )
4		simpr	⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑁 ⊆ 𝑠 ) → 𝑁 ⊆ 𝑠 )
5		simplr	⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑁 ⊆ 𝑠 ) → 𝑠 ∈ 𝒫 𝑋 )
6	5	elpwid	⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑁 ⊆ 𝑠 ) → 𝑠 ⊆ 𝑋 )
7	1	ssnei2	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) ∧ ( 𝑁 ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑋 ) ) → 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) )
8	3 4 6 7	syl12anc	⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑁 ⊆ 𝑠 ) → 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) )
9	8	exp31	⊢ ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) → ( 𝑠 ∈ 𝒫 𝑋 → ( 𝑁 ⊆ 𝑠 → 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) ) )
10	9	ralrimiv	⊢ ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) → ∀ 𝑠 ∈ 𝒫 𝑋 ( 𝑁 ⊆ 𝑠 → 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) )