Metamath Proof Explorer


Theorem sepnsepo

Description: Open neighborhood and neighborhood is equivalent regarding disjointness for both sides. Namely, separatedness by open neighborhoods is equivalent to separatedness by neighborhoods. (Contributed by Zhi Wang, 1-Sep-2024)

Ref Expression
Hypothesis sepnsepolem2.1 ( 𝜑𝐽 ∈ Top )
Assertion sepnsepo ( 𝜑 → ( ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐷 ) ( 𝑥𝑦 ) = ∅ ↔ ∃ 𝑥𝐽𝑦𝐽 ( 𝐶𝑥𝐷𝑦 ∧ ( 𝑥𝑦 ) = ∅ ) ) )

Proof

Step Hyp Ref Expression
1 sepnsepolem2.1 ( 𝜑𝐽 ∈ Top )
2 id ( 𝐽 ∈ Top → 𝐽 ∈ Top )
3 2 sepnsepolem2 ( 𝐽 ∈ Top → ( ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐷 ) ( 𝑥𝑦 ) = ∅ ↔ ∃ 𝑦𝐽 ( 𝐷𝑦 ∧ ( 𝑥𝑦 ) = ∅ ) ) )
4 3 anbi2d ( 𝐽 ∈ Top → ( ( 𝐶𝑥 ∧ ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐷 ) ( 𝑥𝑦 ) = ∅ ) ↔ ( 𝐶𝑥 ∧ ∃ 𝑦𝐽 ( 𝐷𝑦 ∧ ( 𝑥𝑦 ) = ∅ ) ) ) )
5 4 rexbidv ( 𝐽 ∈ Top → ( ∃ 𝑥𝐽 ( 𝐶𝑥 ∧ ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐷 ) ( 𝑥𝑦 ) = ∅ ) ↔ ∃ 𝑥𝐽 ( 𝐶𝑥 ∧ ∃ 𝑦𝐽 ( 𝐷𝑦 ∧ ( 𝑥𝑦 ) = ∅ ) ) ) )
6 ssrin ( 𝑧𝑥 → ( 𝑧𝑦 ) ⊆ ( 𝑥𝑦 ) )
7 sseq0 ( ( ( 𝑧𝑦 ) ⊆ ( 𝑥𝑦 ) ∧ ( 𝑥𝑦 ) = ∅ ) → ( 𝑧𝑦 ) = ∅ )
8 7 ex ( ( 𝑧𝑦 ) ⊆ ( 𝑥𝑦 ) → ( ( 𝑥𝑦 ) = ∅ → ( 𝑧𝑦 ) = ∅ ) )
9 6 8 syl ( 𝑧𝑥 → ( ( 𝑥𝑦 ) = ∅ → ( 𝑧𝑦 ) = ∅ ) )
10 9 adantl ( ( 𝐽 ∈ Top ∧ 𝑧𝑥 ) → ( ( 𝑥𝑦 ) = ∅ → ( 𝑧𝑦 ) = ∅ ) )
11 10 reximdv ( ( 𝐽 ∈ Top ∧ 𝑧𝑥 ) → ( ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐷 ) ( 𝑥𝑦 ) = ∅ → ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐷 ) ( 𝑧𝑦 ) = ∅ ) )
12 simpr ( ( 𝐽 ∈ Top ∧ 𝑥 = 𝑧 ) → 𝑥 = 𝑧 )
13 12 ineq1d ( ( 𝐽 ∈ Top ∧ 𝑥 = 𝑧 ) → ( 𝑥𝑦 ) = ( 𝑧𝑦 ) )
14 13 eqeq1d ( ( 𝐽 ∈ Top ∧ 𝑥 = 𝑧 ) → ( ( 𝑥𝑦 ) = ∅ ↔ ( 𝑧𝑦 ) = ∅ ) )
15 14 rexbidv ( ( 𝐽 ∈ Top ∧ 𝑥 = 𝑧 ) → ( ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐷 ) ( 𝑥𝑦 ) = ∅ ↔ ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐷 ) ( 𝑧𝑦 ) = ∅ ) )
16 2 11 15 opnneieqv ( 𝐽 ∈ Top → ( ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐷 ) ( 𝑥𝑦 ) = ∅ ↔ ∃ 𝑥𝐽 ( 𝐶𝑥 ∧ ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐷 ) ( 𝑥𝑦 ) = ∅ ) ) )
17 sepnsepolem1 ( ∃ 𝑥𝐽𝑦𝐽 ( 𝐶𝑥𝐷𝑦 ∧ ( 𝑥𝑦 ) = ∅ ) ↔ ∃ 𝑥𝐽 ( 𝐶𝑥 ∧ ∃ 𝑦𝐽 ( 𝐷𝑦 ∧ ( 𝑥𝑦 ) = ∅ ) ) )
18 17 a1i ( 𝐽 ∈ Top → ( ∃ 𝑥𝐽𝑦𝐽 ( 𝐶𝑥𝐷𝑦 ∧ ( 𝑥𝑦 ) = ∅ ) ↔ ∃ 𝑥𝐽 ( 𝐶𝑥 ∧ ∃ 𝑦𝐽 ( 𝐷𝑦 ∧ ( 𝑥𝑦 ) = ∅ ) ) ) )
19 5 16 18 3bitr4d ( 𝐽 ∈ Top → ( ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐷 ) ( 𝑥𝑦 ) = ∅ ↔ ∃ 𝑥𝐽𝑦𝐽 ( 𝐶𝑥𝐷𝑦 ∧ ( 𝑥𝑦 ) = ∅ ) ) )
20 1 19 syl ( 𝜑 → ( ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐷 ) ( 𝑥𝑦 ) = ∅ ↔ ∃ 𝑥𝐽𝑦𝐽 ( 𝐶𝑥𝐷𝑦 ∧ ( 𝑥𝑦 ) = ∅ ) ) )