Metamath Proof Explorer

Theorem dfnrm3

Description: A topological space is normal if any disjoint closed sets can be separated by neighborhoods. An alternate definition of df-nrm . (Contributed by Zhi Wang, 2-Sep-2024)

Ref Expression
Assertion dfnrm3 ⊢ 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 isnrm4 ⊢ j ∈ Nrm ↔ j ∈ Top ∧ ∀ c ∈ Clsd ⁡ j ∀ d ∈ Clsd ⁡ j c ∩ d = ∅ → ∃ x ∈ nei ⁡ j ⁡ c ∃ y ∈ nei ⁡ j ⁡ d x ∩ y = ∅
2 1 abbi2i ⊢ Nrm = j | j ∈ Top ∧ ∀ c ∈ Clsd ⁡ j ∀ d ∈ Clsd ⁡ j c ∩ d = ∅ → ∃ x ∈ nei ⁡ j ⁡ c ∃ y ∈ nei ⁡ j ⁡ d x ∩ y = ∅
3 df-rab ⊢ j ∈ Top | ∀ c ∈ Clsd ⁡ j ∀ d ∈ Clsd ⁡ j c ∩ d = ∅ → ∃ x ∈ nei ⁡ j ⁡ c ∃ y ∈ nei ⁡ j ⁡ d x ∩ y = ∅ = j | j ∈ Top ∧ ∀ c ∈ Clsd ⁡ j ∀ d ∈ Clsd ⁡ j c ∩ d = ∅ → ∃ x ∈ nei ⁡ j ⁡ c ∃ y ∈ nei ⁡ j ⁡ d x ∩ y = ∅
4 2 3 eqtr4i ⊢ Nrm = j ∈ Top | ∀ c ∈ Clsd ⁡ j ∀ d ∈ Clsd ⁡ j c ∩ d = ∅ → ∃ x ∈ nei ⁡ j ⁡ c ∃ y ∈ nei ⁡ j ⁡ d x ∩ y = ∅