Metamath Proof Explorer

Theorem iscnrm4

Description: A completely normal topology is a topology in which two separated sets can be separated by neighborhoods. (Contributed by Zhi Wang, 5-Sep-2024)

		Ref	Expression
	Assertion	iscnrm4	$⊢ 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 nei (J) (s) \exists m \in nei (J) (t) 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		id	$⊢ J \in Top \to J \in Top$
3	2	sepnsepo	$⊢ J \in Top \to (\exists n \in nei (J) (s) \exists m \in nei (J) (t) n \cap m = \emptyset \leftrightarrow \exists n \in J \exists m \in J (s \subseteq n \land t \subseteq m \land n \cap m = \emptyset))$
4	3	imbi2d	$⊢ J \in Top \to (((s \cap cls (J) (t) = \emptyset \land cls (J) (s) \cap t = \emptyset) \to \exists n \in nei (J) (s) \exists m \in nei (J) (t) n \cap m = \emptyset) \leftrightarrow ((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)))$
5	4	2ralbidv	$⊢ J \in Top \to (\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 nei (J) (s) \exists m \in nei (J) (t) n \cap m = \emptyset) \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)))$
6	5	pm5.32i	$⊢ (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 nei (J) (s) \exists m \in nei (J) (t) n \cap m = \emptyset)) \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)))$
7	1 6	bitr4i	$⊢ 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 nei (J) (s) \exists m \in nei (J) (t) n \cap m = \emptyset))$