Theorem opnneirv

Description: A variant of opnneir with different dummy variables. (Contributed by Zhi Wang, 31-Aug-2024)

	Ref	Expression
Hypotheses	opnneir.1	$$⊢\phi \to J\in \mathrm{Top}$$
	opnneirv.2	$$⊢\left(\phi \wedge x=y\right)\to \left(\psi \leftrightarrow \chi \right)$$
Assertion	opnneirv	$$⊢\phi \to \left(\exists x\in J\left(S\subseteq x\wedge \psi \right)\to \exists y\in \mathrm{nei}\left(J\right)\left(S\right)\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		opnneir.1	$$⊢\phi \to J\in \mathrm{Top}$$
2		opnneirv.2	$$⊢\left(\phi \wedge x=y\right)\to \left(\psi \leftrightarrow \chi \right)$$
3	2	opnneilem	$$⊢\phi \to \left(\exists x\in J\left(S\subseteq x\wedge \psi \right)\leftrightarrow \exists y\in J\left(S\subseteq y\wedge \chi \right)\right)$$
4	1	opnneir	$$⊢\phi \to \left(\exists y\in J\left(S\subseteq y\wedge \chi \right)\to \exists y\in \mathrm{nei}\left(J\right)\left(S\right)\chi \right)$$
5	3 4	sylbid	$$⊢\phi \to \left(\exists x\in J\left(S\subseteq x\wedge \psi \right)\to \exists y\in \mathrm{nei}\left(J\right)\left(S\right)\chi \right)$$