Metamath Proof Explorer

Theorem isnrm4

Description: A topological space is normal iff any two disjoint closed sets are separated by neighborhoods. (Contributed by Zhi Wang, 1-Sep-2024)

Ref Expression
Assertion isnrm4 ⊢ J ∈ Nrm ↔ J ∈ Top ∧ ∀ c ∈ Clsd ⁡ J ∀ d ∈ Clsd ⁡ J c ∩ d = ∅ → ∃ x ∈ nei ⁡ J ⁡ c ∃ y ∈ nei ⁡ J ⁡ d x ∩ y = ∅

Proof

Step Hyp Ref Expression
1 isnrm3 ⊢ J ∈ Nrm ↔ J ∈ Top ∧ ∀ c ∈ Clsd ⁡ J ∀ d ∈ Clsd ⁡ J c ∩ d = ∅ → ∃ x ∈ J ∃ y ∈ J c ⊆ x ∧ d ⊆ y ∧ x ∩ y = ∅
2 id ⊢ J ∈ Top → J ∈ Top
3 2 sepnsepo ⊢ J ∈ Top → ∃ x ∈ nei ⁡ J ⁡ c ∃ y ∈ nei ⁡ J ⁡ d x ∩ y = ∅ ↔ ∃ x ∈ J ∃ y ∈ J c ⊆ x ∧ d ⊆ y ∧ x ∩ y = ∅
4 3 imbi2d ⊢ J ∈ Top → c ∩ d = ∅ → ∃ x ∈ nei ⁡ J ⁡ c ∃ y ∈ nei ⁡ J ⁡ d x ∩ y = ∅ ↔ c ∩ d = ∅ → ∃ x ∈ J ∃ y ∈ J c ⊆ x ∧ d ⊆ y ∧ x ∩ y = ∅
5 4 2ralbidv ⊢ J ∈ Top → ∀ c ∈ Clsd ⁡ J ∀ d ∈ Clsd ⁡ J c ∩ d = ∅ → ∃ x ∈ nei ⁡ J ⁡ c ∃ y ∈ nei ⁡ J ⁡ d x ∩ y = ∅ ↔ ∀ c ∈ Clsd ⁡ J ∀ d ∈ Clsd ⁡ J c ∩ d = ∅ → ∃ x ∈ J ∃ y ∈ J c ⊆ x ∧ d ⊆ y ∧ x ∩ y = ∅
6 5 pm5.32i ⊢ J ∈ Top ∧ ∀ c ∈ Clsd ⁡ J ∀ d ∈ Clsd ⁡ J c ∩ d = ∅ → ∃ x ∈ nei ⁡ J ⁡ c ∃ y ∈ nei ⁡ J ⁡ d x ∩ y = ∅ ↔ J ∈ Top ∧ ∀ c ∈ Clsd ⁡ J ∀ d ∈ Clsd ⁡ J c ∩ d = ∅ → ∃ x ∈ J ∃ y ∈ J c ⊆ x ∧ d ⊆ y ∧ x ∩ y = ∅
7 1 6 bitr4i ⊢ J ∈ Nrm ↔ J ∈ Top ∧ ∀ c ∈ Clsd ⁡ J ∀ d ∈ Clsd ⁡ J c ∩ d = ∅ → ∃ x ∈ nei ⁡ J ⁡ c ∃ y ∈ nei ⁡ J ⁡ d x ∩ y = ∅