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

Proof

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