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⁡jc∩d=∅→∃x∈j∃y∈jc⊆x∧d⊆y∧x∩y=∅

Proof

Step Hyp Ref Expression
1 isnrm3 ⊢j∈Nrm↔j∈Top∧∀c∈Clsd⁡j∀d∈Clsd⁡jc∩d=∅→∃x∈j∃y∈jc⊆x∧d⊆y∧x∩y=∅
2 1 eqabi ⊢Nrm=j|j∈Top∧∀c∈Clsd⁡j∀d∈Clsd⁡jc∩d=∅→∃x∈j∃y∈jc⊆x∧d⊆y∧x∩y=∅
3 df-rab ⊢j∈Top|∀c∈Clsd⁡j∀d∈Clsd⁡jc∩d=∅→∃x∈j∃y∈jc⊆x∧d⊆y∧x∩y=∅=j|j∈Top∧∀c∈Clsd⁡j∀d∈Clsd⁡jc∩d=∅→∃x∈j∃y∈jc⊆x∧d⊆y∧x∩y=∅
4 2 3 eqtr4i ⊢Nrm=j∈Top|∀c∈Clsd⁡j∀d∈Clsd⁡jc∩d=∅→∃x∈j∃y∈jc⊆x∧d⊆y∧x∩y=∅