Metamath Proof Explorer


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=J
Assertion gneispb JTopPXNneiJPs𝒫XNssneiJP

Proof

Step Hyp Ref Expression
1 gneispace.x X=J
2 3simpb JTopPXNneiJPJTopNneiJP
3 2 ad2antrr JTopPXNneiJPs𝒫XNsJTopNneiJP
4 simpr JTopPXNneiJPs𝒫XNsNs
5 simplr JTopPXNneiJPs𝒫XNss𝒫X
6 5 elpwid JTopPXNneiJPs𝒫XNssX
7 1 ssnei2 JTopNneiJPNssXsneiJP
8 3 4 6 7 syl12anc JTopPXNneiJPs𝒫XNssneiJP
9 8 exp31 JTopPXNneiJPs𝒫XNssneiJP
10 9 ralrimiv JTopPXNneiJPs𝒫XNssneiJP