Description: The equivalence between neighborhood and open neighborhood. A variant of opnneieqv with two dummy variables. (Contributed by Zhi Wang, 31-Aug-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | opnneir.1 | ⊢ ( 𝜑 → 𝐽 ∈ Top ) | |
opnneilv.2 | ⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝑥 ) → ( 𝜓 → 𝜒 ) ) | ||
opnneil.3 | ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → ( 𝜓 ↔ 𝜒 ) ) | ||
Assertion | opnneieqvv | ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) 𝜓 ↔ ∃ 𝑦 ∈ 𝐽 ( 𝑆 ⊆ 𝑦 ∧ 𝜒 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opnneir.1 | ⊢ ( 𝜑 → 𝐽 ∈ Top ) | |
2 | opnneilv.2 | ⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝑥 ) → ( 𝜓 → 𝜒 ) ) | |
3 | opnneil.3 | ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → ( 𝜓 ↔ 𝜒 ) ) | |
4 | 1 2 3 | opnneieqv | ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) 𝜓 ↔ ∃ 𝑥 ∈ 𝐽 ( 𝑆 ⊆ 𝑥 ∧ 𝜓 ) ) ) |
5 | 3 | opnneilem | ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐽 ( 𝑆 ⊆ 𝑥 ∧ 𝜓 ) ↔ ∃ 𝑦 ∈ 𝐽 ( 𝑆 ⊆ 𝑦 ∧ 𝜒 ) ) ) |
6 | 4 5 | bitrd | ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) 𝜓 ↔ ∃ 𝑦 ∈ 𝐽 ( 𝑆 ⊆ 𝑦 ∧ 𝜒 ) ) ) |