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 opnneibid ⊢ ( 𝐽 ∈ Top → ( ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐷 ) ( 𝑥 ∩ 𝑦 ) = ∅ ↔ ∃ 𝑥 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐷 ) ( 𝑥 ∩ 𝑦 ) = ∅ ) ) )
17 sepnsepolem1 ⊢ ( ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ 𝐷 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ↔ ∃ 𝑥 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ ∃ 𝑦 ∈ 𝐽 ( 𝐷 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) )
18 17 a1i ⊢ ( 𝐽 ∈ Top → ( ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ 𝐷 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ↔ ∃ 𝑥 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ ∃ 𝑦 ∈ 𝐽 ( 𝐷 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ) )
19 5 16 18 3bitr4d ⊢ ( 𝐽 ∈ Top → ( ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐷 ) ( 𝑥 ∩ 𝑦 ) = ∅ ↔ ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ 𝐷 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) )
20 1 19 syl ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐷 ) ( 𝑥 ∩ 𝑦 ) = ∅ ↔ ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ 𝐷 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) )