opnneir

Description: If something is true for an open neighborhood, it must be true for a neighborhood. (Contributed by Zhi Wang, 31-Aug-2024)

		Ref	Expression
	Hypothesis	opnneir.1	$⊢ φ \to J \in Top$
	Assertion	opnneir	$⊢ φ \to (\exists x \in J (S \subseteq x \land ψ) \to \exists x \in nei (J) (S) ψ)$

Step	Hyp	Ref	Expression
1		opnneir.1	$⊢ φ \to J \in Top$
2		anass	$⊢ ((x \in J \land S \subseteq x) \land ψ) \leftrightarrow (x \in J \land (S \subseteq x \land ψ))$
3		opnneiss	$⊢ (J \in Top \land x \in J \land S \subseteq x) \to x \in nei (J) (S)$
4	3	3expib	$⊢ J \in Top \to ((x \in J \land S \subseteq x) \to x \in nei (J) (S))$
5	4	anim1d	$⊢ J \in Top \to (((x \in J \land S \subseteq x) \land ψ) \to (x \in nei (J) (S) \land ψ))$
6	2 5	syl5bir	$⊢ J \in Top \to ((x \in J \land (S \subseteq x \land ψ)) \to (x \in nei (J) (S) \land ψ))$
7	6	reximdv2	$⊢ J \in Top \to (\exists x \in J (S \subseteq x \land ψ) \to \exists x \in nei (J) (S) ψ)$
8	1 7	syl	$⊢ φ \to (\exists x \in J (S \subseteq x \land ψ) \to \exists x \in nei (J) (S) ψ)$

Metamath Proof Explorer