Metamath Proof Explorer


Theorem opnneil

Description: A variant of opnneilv . (Contributed by Zhi Wang, 31-Aug-2024)

Ref Expression
Hypotheses opnneir.1 ( 𝜑𝐽 ∈ Top )
opnneilv.2 ( ( 𝜑𝑦𝑥 ) → ( 𝜓𝜒 ) )
opnneil.3 ( ( 𝜑𝑥 = 𝑦 ) → ( 𝜓𝜒 ) )
Assertion opnneil ( 𝜑 → ( ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) 𝜓 → ∃ 𝑥𝐽 ( 𝑆𝑥𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 opnneir.1 ( 𝜑𝐽 ∈ Top )
2 opnneilv.2 ( ( 𝜑𝑦𝑥 ) → ( 𝜓𝜒 ) )
3 opnneil.3 ( ( 𝜑𝑥 = 𝑦 ) → ( 𝜓𝜒 ) )
4 1 2 opnneilv ( 𝜑 → ( ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) 𝜓 → ∃ 𝑦𝐽 ( 𝑆𝑦𝜒 ) ) )
5 3 opnneilem ( 𝜑 → ( ∃ 𝑥𝐽 ( 𝑆𝑥𝜓 ) ↔ ∃ 𝑦𝐽 ( 𝑆𝑦𝜒 ) ) )
6 4 5 sylibrd ( 𝜑 → ( ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) 𝜓 → ∃ 𝑥𝐽 ( 𝑆𝑥𝜓 ) ) )