Metamath Proof Explorer

Theorem iscnrm3

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

		Ref	Expression
	Assertion	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)))$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ ⋃ J = ⋃ J$
2	1	iscnrm	$⊢ J \in CNrm \leftrightarrow (J \in Top \land \forall z \in 𝒫 ⋃ J J ↾_{𝑡} z \in Nrm)$
3		iscnrm3lem1	$⊢ J \in Top \to (\forall z \in 𝒫 ⋃ J \forall c \in Clsd (J ↾_{𝑡} z) \forall d \in Clsd (J ↾_{𝑡} z) (c \cap d = \emptyset \to \exists l \in (J ↾_{𝑡} z) \exists k \in (J ↾_{𝑡} z) (c \subseteq l \land d \subseteq k \land l \cap k = \emptyset)) \leftrightarrow \forall z \in 𝒫 ⋃ J (J ↾_{𝑡} z \in Top \land \forall c \in Clsd (J ↾_{𝑡} z) \forall d \in Clsd (J ↾_{𝑡} z) (c \cap d = \emptyset \to \exists l \in (J ↾_{𝑡} z) \exists k \in (J ↾_{𝑡} z) (c \subseteq l \land d \subseteq k \land l \cap k = \emptyset))))$
4		isnrm3	$⊢ J ↾_{𝑡} z \in Nrm \leftrightarrow (J ↾_{𝑡} z \in Top \land \forall c \in Clsd (J ↾_{𝑡} z) \forall d \in Clsd (J ↾_{𝑡} z) (c \cap d = \emptyset \to \exists l \in (J ↾_{𝑡} z) \exists k \in (J ↾_{𝑡} z) (c \subseteq l \land d \subseteq k \land l \cap k = \emptyset)))$
5	4	ralbii	$⊢ \forall z \in 𝒫 ⋃ J J ↾_{𝑡} z \in Nrm \leftrightarrow \forall z \in 𝒫 ⋃ J (J ↾_{𝑡} z \in Top \land \forall c \in Clsd (J ↾_{𝑡} z) \forall d \in Clsd (J ↾_{𝑡} z) (c \cap d = \emptyset \to \exists l \in (J ↾_{𝑡} z) \exists k \in (J ↾_{𝑡} z) (c \subseteq l \land d \subseteq k \land l \cap k = \emptyset)))$
6	3 5	bitr4di	$⊢ J \in Top \to (\forall z \in 𝒫 ⋃ J \forall c \in Clsd (J ↾_{𝑡} z) \forall d \in Clsd (J ↾_{𝑡} z) (c \cap d = \emptyset \to \exists l \in (J ↾_{𝑡} z) \exists k \in (J ↾_{𝑡} z) (c \subseteq l \land d \subseteq k \land l \cap k = \emptyset)) \leftrightarrow \forall z \in 𝒫 ⋃ J J ↾_{𝑡} z \in Nrm)$
7		iscnrm3r	$⊢ J \in Top \to (\forall z \in 𝒫 ⋃ J \forall c \in Clsd (J ↾_{𝑡} z) \forall d \in Clsd (J ↾_{𝑡} z) (c \cap d = \emptyset \to \exists l \in (J ↾_{𝑡} z) \exists k \in (J ↾_{𝑡} z) (c \subseteq l \land d \subseteq k \land l \cap k = \emptyset)) \to ((s \in 𝒫 ⋃ J \land t \in 𝒫 ⋃ J) \to ((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))))$
8		iscnrm3l	$⊢ 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 J \exists m \in J (s \subseteq n \land t \subseteq m \land n \cap m = \emptyset)) \to ((z \in 𝒫 ⋃ J \land c \in Clsd (J ↾_{𝑡} z) \land d \in Clsd (J ↾_{𝑡} z)) \to (c \cap d = \emptyset \to \exists l \in (J ↾_{𝑡} z) \exists k \in (J ↾_{𝑡} z) (c \subseteq l \land d \subseteq k \land l \cap k = \emptyset))))$
9	7 8	iscnrm3lem2	$⊢ J \in Top \to (\forall z \in 𝒫 ⋃ J \forall c \in Clsd (J ↾_{𝑡} z) \forall d \in Clsd (J ↾_{𝑡} z) (c \cap d = \emptyset \to \exists l \in (J ↾_{𝑡} z) \exists k \in (J ↾_{𝑡} z) (c \subseteq l \land d \subseteq k \land l \cap k = \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)))$
10	6 9	bitr3d	$⊢ J \in Top \to (\forall z \in 𝒫 ⋃ J J ↾_{𝑡} z \in Nrm \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)))$
11	10	pm5.32i	$⊢ (J \in Top \land \forall z \in 𝒫 ⋃ J J ↾_{𝑡} z \in Nrm) \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)))$
12	2 11	bitri	$⊢ 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)))$