Description: A variant of opnneir with different dummy variables. (Contributed by Zhi Wang, 31-Aug-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | opnneir.1 | ⊢ ( 𝜑 → 𝐽 ∈ Top ) | |
opnneirv.2 | ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → ( 𝜓 ↔ 𝜒 ) ) | ||
Assertion | opnneirv | ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐽 ( 𝑆 ⊆ 𝑥 ∧ 𝜓 ) → ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) 𝜒 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opnneir.1 | ⊢ ( 𝜑 → 𝐽 ∈ Top ) | |
2 | opnneirv.2 | ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → ( 𝜓 ↔ 𝜒 ) ) | |
3 | 2 | opnneilem | ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐽 ( 𝑆 ⊆ 𝑥 ∧ 𝜓 ) ↔ ∃ 𝑦 ∈ 𝐽 ( 𝑆 ⊆ 𝑦 ∧ 𝜒 ) ) ) |
4 | 1 | opnneir | ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝐽 ( 𝑆 ⊆ 𝑦 ∧ 𝜒 ) → ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) 𝜒 ) ) |
5 | 3 4 | sylbid | ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐽 ( 𝑆 ⊆ 𝑥 ∧ 𝜓 ) → ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) 𝜒 ) ) |