Metamath Proof Explorer

Theorem dfnrm2

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

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