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 \in Top \to (J \in CNrm \leftrightarrow \forall s \in 𝒫 ⋃ J \forall t \in 𝒫 ⋃ J ((s \cap cls (J) (t) = \emptyset \land cls (J) (s) \cap t = \emptyset) \to \exists n \in J \exists m \in J (s \subseteq n \land t \subseteq m \land n \cap m = \emptyset)))$

Proof

Step	Hyp	Ref	Expression
1		iscnrm3	$⊢ J \in CNrm \leftrightarrow (J \in Top \land \forall s \in 𝒫 ⋃ J \forall t \in 𝒫 ⋃ J ((s \cap cls (J) (t) = \emptyset \land cls (J) (s) \cap t = \emptyset) \to \exists n \in J \exists m \in J (s \subseteq n \land t \subseteq m \land n \cap m = \emptyset)))$
2	1	baib	$⊢ J \in Top \to (J \in CNrm \leftrightarrow \forall s \in 𝒫 ⋃ J \forall t \in 𝒫 ⋃ J ((s \cap cls (J) (t) = \emptyset \land cls (J) (s) \cap t = \emptyset) \to \exists n \in J \exists m \in J (s \subseteq n \land t \subseteq m \land n \cap m = \emptyset)))$