iscnrm3l

Description: Lemma for iscnrm3 . Given a topology J , if two separated sets can be separated by open neighborhoods, then all subspaces of the topology J are normal, i.e., two disjoint closed sets can be separated by open neighborhoods. (Contributed by Zhi Wang, 5-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (s = C \land t = D) \to s = C$
2		simpr	$⊢ (s = C \land t = D) \to t = D$
3	2	fveq2d	$⊢ (s = C \land t = D) \to cls (J) (t) = cls (J) (D)$
4	1 3	ineq12d	$⊢ (s = C \land t = D) \to s \cap cls (J) (t) = C \cap cls (J) (D)$
5	4	eqeq1d	$⊢ (s = C \land t = D) \to (s \cap cls (J) (t) = \emptyset \leftrightarrow C \cap cls (J) (D) = \emptyset)$
6	1	fveq2d	$⊢ (s = C \land t = D) \to cls (J) (s) = cls (J) (C)$
7	6 2	ineq12d	$⊢ (s = C \land t = D) \to cls (J) (s) \cap t = cls (J) (C) \cap D$
8	7	eqeq1d	$⊢ (s = C \land t = D) \to (cls (J) (s) \cap t = \emptyset \leftrightarrow cls (J) (C) \cap D = \emptyset)$
9	5 8	anbi12d	$⊢ (s = C \land t = D) \to ((s \cap cls (J) (t) = \emptyset \land cls (J) (s) \cap t = \emptyset) \leftrightarrow (C \cap cls (J) (D) = \emptyset \land cls (J) (C) \cap D = \emptyset))$
10	1	sseq1d	$⊢ (s = C \land t = D) \to (s \subseteq n \leftrightarrow C \subseteq n)$
11	2	sseq1d	$⊢ (s = C \land t = D) \to (t \subseteq m \leftrightarrow D \subseteq m)$
12	10 11	3anbi12d	$⊢ (s = C \land t = D) \to ((s \subseteq n \land t \subseteq m \land n \cap m = \emptyset) \leftrightarrow (C \subseteq n \land D \subseteq m \land n \cap m = \emptyset))$
13	12	2rexbidv	$⊢ (s = C \land t = D) \to (\exists n \in J \exists m \in J (s \subseteq n \land t \subseteq m \land n \cap m = \emptyset) \leftrightarrow \exists n \in J \exists m \in J (C \subseteq n \land D \subseteq m \land n \cap m = \emptyset))$
14		iscnrm3llem1	$⊢ (J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \to (C \in 𝒫 ⋃ J \land D \in 𝒫 ⋃ J)$
15		simp1	$⊢ (J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \to J \in Top$
16		eqidd	$⊢ (J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \to ⋃ J = ⋃ J$
17		simp21	$⊢ (J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \to Z \in 𝒫 ⋃ J$
18	17	elpwid	$⊢ (J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \to Z \subseteq ⋃ J$
19		eqidd	$⊢ (J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \to J ↾_{𝑡} Z = J ↾_{𝑡} Z$
20		simp22	$⊢ (J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \to C \in Clsd (J ↾_{𝑡} Z)$
21		simp3	$⊢ (J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \to C \cap D = \emptyset$
22		simp23	$⊢ (J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \to D \in Clsd (J ↾_{𝑡} Z)$
23	15 16 18 19 20 21 22	restclssep	$⊢ (J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \to (C \cap cls (J) (D) = \emptyset \land cls (J) (C) \cap D = \emptyset)$
24		iscnrm3llem2	$⊢ (J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \to (\exists n \in J \exists m \in J (C \subseteq n \land D \subseteq m \land n \cap m = \emptyset) \to \exists l \in (J ↾_{𝑡} Z) \exists k \in (J ↾_{𝑡} Z) (C \subseteq l \land D \subseteq k \land l \cap k = \emptyset))$
25	23 24	embantd	$⊢ (J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \to (((C \cap cls (J) (D) = \emptyset \land cls (J) (C) \cap D = \emptyset) \to \exists n \in J \exists m \in J (C \subseteq n \land D \subseteq m \land n \cap m = \emptyset)) \to \exists l \in (J ↾_{𝑡} Z) \exists k \in (J ↾_{𝑡} Z) (C \subseteq l \land D \subseteq k \land l \cap k = \emptyset))$
26	9 13 14 25	iscnrm3lem5	$⊢ 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))))$

Metamath Proof Explorer

Theorem iscnrm3l

Proof