Metamath Proof Explorer

Theorem sepcsepo

Description: If two sets are separated by closed neighborhoods, then they are separated by (open) neighborhoods. See sepnsepo for the equivalence between separatedness by open neighborhoods and separatedness by neighborhoods. Although J e. Top might be redundant here, it is listed for explicitness. J e. Top can be obtained from neircl , adantr , and rexlimiva . (Contributed by Zhi Wang, 8-Sep-2024)

Ref Expression
Hypotheses sepdisj.1 ⊢ φ → J ∈ Top
sepcsepo.2 ⊢ φ → ∃ n ∈ nei ⁡ J ⁡ S ∃ m ∈ nei ⁡ J ⁡ T n ∈ Clsd ⁡ J ∧ m ∈ Clsd ⁡ J ∧ n ∩ m = ∅
Assertion sepcsepo ⊢ φ → ∃ n ∈ J ∃ m ∈ J S ⊆ n ∧ T ⊆ m ∧ n ∩ m = ∅

Proof

Step Hyp Ref Expression
1 sepdisj.1 ⊢ φ → J ∈ Top
2 sepcsepo.2 ⊢ φ → ∃ n ∈ nei ⁡ J ⁡ S ∃ m ∈ nei ⁡ J ⁡ T n ∈ Clsd ⁡ J ∧ m ∈ Clsd ⁡ J ∧ n ∩ m = ∅
3 simp3 ⊢ n ∈ Clsd ⁡ J ∧ m ∈ Clsd ⁡ J ∧ n ∩ m = ∅ → n ∩ m = ∅
4 3 reximi ⊢ ∃ m ∈ nei ⁡ J ⁡ T n ∈ Clsd ⁡ J ∧ m ∈ Clsd ⁡ J ∧ n ∩ m = ∅ → ∃ m ∈ nei ⁡ J ⁡ T n ∩ m = ∅
5 4 reximi ⊢ ∃ n ∈ nei ⁡ J ⁡ S ∃ m ∈ nei ⁡ J ⁡ T n ∈ Clsd ⁡ J ∧ m ∈ Clsd ⁡ J ∧ n ∩ m = ∅ → ∃ n ∈ nei ⁡ J ⁡ S ∃ m ∈ nei ⁡ J ⁡ T n ∩ m = ∅
6 2 5 syl ⊢ φ → ∃ n ∈ nei ⁡ J ⁡ S ∃ m ∈ nei ⁡ J ⁡ T n ∩ m = ∅
7 1 sepnsepo ⊢ φ → ∃ n ∈ nei ⁡ J ⁡ S ∃ m ∈ nei ⁡ J ⁡ T n ∩ m = ∅ ↔ ∃ n ∈ J ∃ m ∈ J S ⊆ n ∧ T ⊆ m ∧ n ∩ m = ∅
8 6 7 mpbid ⊢ φ → ∃ n ∈ J ∃ m ∈ J S ⊆ n ∧ T ⊆ m ∧ n ∩ m = ∅