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	$⊢ (J \in Top \land P \in X \land N \in nei (J) (\{P\})) \to \forall s \in 𝒫 X (N \subseteq s \to s \in nei (J) (\{P\}))$

Proof

Step	Hyp	Ref	Expression
1		gneispace.x	$⊢ X = ⋃ J$
2		3simpb	$⊢ (J \in Top \land P \in X \land N \in nei (J) (\{P\})) \to (J \in Top \land N \in nei (J) (\{P\}))$
3	2	ad2antrr	$⊢ (((J \in Top \land P \in X \land N \in nei (J) (\{P\})) \land s \in 𝒫 X) \land N \subseteq s) \to (J \in Top \land N \in nei (J) (\{P\}))$
4		simpr	$⊢ (((J \in Top \land P \in X \land N \in nei (J) (\{P\})) \land s \in 𝒫 X) \land N \subseteq s) \to N \subseteq s$
5		simplr	$⊢ (((J \in Top \land P \in X \land N \in nei (J) (\{P\})) \land s \in 𝒫 X) \land N \subseteq s) \to s \in 𝒫 X$
6	5	elpwid	$⊢ (((J \in Top \land P \in X \land N \in nei (J) (\{P\})) \land s \in 𝒫 X) \land N \subseteq s) \to s \subseteq X$
7	1	ssnei2	$⊢ ((J \in Top \land N \in nei (J) (\{P\})) \land (N \subseteq s \land s \subseteq X)) \to s \in nei (J) (\{P\})$
8	3 4 6 7	syl12anc	$⊢ (((J \in Top \land P \in X \land N \in nei (J) (\{P\})) \land s \in 𝒫 X) \land N \subseteq s) \to s \in nei (J) (\{P\})$
9	8	exp31	$⊢ (J \in Top \land P \in X \land N \in nei (J) (\{P\})) \to (s \in 𝒫 X \to (N \subseteq s \to s \in nei (J) (\{P\})))$
10	9	ralrimiv	$⊢ (J \in Top \land P \in X \land N \in nei (J) (\{P\})) \to \forall s \in 𝒫 X (N \subseteq s \to s \in nei (J) (\{P\}))$