Metamath Proof Explorer


Theorem iscnrm3v

Description: A topology is completely normal iff two separated sets can be separated by open neighborhoods. (Contributed by Zhi Wang, 10-Sep-2024)

Ref Expression
Assertion iscnrm3v J Top J CNrm s 𝒫 J t 𝒫 J s cls J t = cls J s t = n J m J s n t m n m =

Proof

Step Hyp Ref Expression
1 iscnrm3 J CNrm J Top s 𝒫 J t 𝒫 J s cls J t = cls J s t = n J m J s n t m n m =
2 1 baib J Top J CNrm s 𝒫 J t 𝒫 J s cls J t = cls J s t = n J m J s n t m n m =