iscnrm3llem2

Description: Lemma for iscnrm3l . If there exist disjoint open neighborhoods in the original topology for two disjoint closed sets in a subspace, then they can be separated by open neighborhoods in the subspace topology. (Could shorten proof with ssin0 .) (Contributed by Zhi Wang, 5-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		sseq2	$⊢ l = n \cap Z \to (C \subseteq l \leftrightarrow C \subseteq n \cap Z)$
2		ineq1	$⊢ l = n \cap Z \to l \cap k = (n \cap Z) \cap k$
3	2	eqeq1d	$⊢ l = n \cap Z \to (l \cap k = \emptyset \leftrightarrow (n \cap Z) \cap k = \emptyset)$
4	1 3	3anbi13d	$⊢ l = n \cap Z \to ((C \subseteq l \land D \subseteq k \land l \cap k = \emptyset) \leftrightarrow (C \subseteq n \cap Z \land D \subseteq k \land (n \cap Z) \cap k = \emptyset))$
5		sseq2	$⊢ k = m \cap Z \to (D \subseteq k \leftrightarrow D \subseteq m \cap Z)$
6		ineq2	$⊢ k = m \cap Z \to (n \cap Z) \cap k = (n \cap Z) \cap (m \cap Z)$
7	6	eqeq1d	$⊢ k = m \cap Z \to ((n \cap Z) \cap k = \emptyset \leftrightarrow (n \cap Z) \cap (m \cap Z) = \emptyset)$
8	5 7	3anbi23d	$⊢ k = m \cap Z \to ((C \subseteq n \cap Z \land D \subseteq k \land (n \cap Z) \cap k = \emptyset) \leftrightarrow (C \subseteq n \cap Z \land D \subseteq m \cap Z \land (n \cap Z) \cap (m \cap Z) = \emptyset))$
9		simp11	$⊢ ((J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \land (n \in J \land m \in J) \land (C \subseteq n \land D \subseteq m \land n \cap m = \emptyset)) \to J \in Top$
10		simp121	$⊢ ((J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \land (n \in J \land m \in J) \land (C \subseteq n \land D \subseteq m \land n \cap m = \emptyset)) \to Z \in 𝒫 ⋃ J$
11		simp2l	$⊢ ((J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \land (n \in J \land m \in J) \land (C \subseteq n \land D \subseteq m \land n \cap m = \emptyset)) \to n \in J$
12		elrestr	$⊢ (J \in Top \land Z \in 𝒫 ⋃ J \land n \in J) \to n \cap Z \in (J ↾_{𝑡} Z)$
13	9 10 11 12	syl3anc	$⊢ ((J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \land (n \in J \land m \in J) \land (C \subseteq n \land D \subseteq m \land n \cap m = \emptyset)) \to n \cap Z \in (J ↾_{𝑡} Z)$
14		simp2r	$⊢ ((J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \land (n \in J \land m \in J) \land (C \subseteq n \land D \subseteq m \land n \cap m = \emptyset)) \to m \in J$
15		elrestr	$⊢ (J \in Top \land Z \in 𝒫 ⋃ J \land m \in J) \to m \cap Z \in (J ↾_{𝑡} Z)$
16	9 10 14 15	syl3anc	$⊢ ((J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \land (n \in J \land m \in J) \land (C \subseteq n \land D \subseteq m \land n \cap m = \emptyset)) \to m \cap Z \in (J ↾_{𝑡} Z)$
17		simp31	$⊢ ((J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \land (n \in J \land m \in J) \land (C \subseteq n \land D \subseteq m \land n \cap m = \emptyset)) \to C \subseteq n$
18		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) \land (n \in J \land m \in J) \land (C \subseteq n \land D \subseteq m \land n \cap m = \emptyset)) \to ⋃ J = ⋃ J$
19	10	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) \land (n \in J \land m \in J) \land (C \subseteq n \land D \subseteq m \land n \cap m = \emptyset)) \to Z \subseteq ⋃ J$
20		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) \land (n \in J \land m \in J) \land (C \subseteq n \land D \subseteq m \land n \cap m = \emptyset)) \to J ↾_{𝑡} Z = J ↾_{𝑡} Z$
21		simp122	$⊢ ((J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \land (n \in J \land m \in J) \land (C \subseteq n \land D \subseteq m \land n \cap m = \emptyset)) \to C \in Clsd (J ↾_{𝑡} Z)$
22	9 18 19 20 21	restcls2lem	$⊢ ((J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \land (n \in J \land m \in J) \land (C \subseteq n \land D \subseteq m \land n \cap m = \emptyset)) \to C \subseteq Z$
23	17 22	ssind	$⊢ ((J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \land (n \in J \land m \in J) \land (C \subseteq n \land D \subseteq m \land n \cap m = \emptyset)) \to C \subseteq n \cap Z$
24		simp32	$⊢ ((J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \land (n \in J \land m \in J) \land (C \subseteq n \land D \subseteq m \land n \cap m = \emptyset)) \to D \subseteq m$
25		simp123	$⊢ ((J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \land (n \in J \land m \in J) \land (C \subseteq n \land D \subseteq m \land n \cap m = \emptyset)) \to D \in Clsd (J ↾_{𝑡} Z)$
26	9 18 19 20 25	restcls2lem	$⊢ ((J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \land (n \in J \land m \in J) \land (C \subseteq n \land D \subseteq m \land n \cap m = \emptyset)) \to D \subseteq Z$
27	24 26	ssind	$⊢ ((J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \land (n \in J \land m \in J) \land (C \subseteq n \land D \subseteq m \land n \cap m = \emptyset)) \to D \subseteq m \cap Z$
28		inss1	$⊢ n \cap Z \subseteq n$
29		inss1	$⊢ m \cap Z \subseteq m$
30		ss2in	$⊢ (n \cap Z \subseteq n \land m \cap Z \subseteq m) \to (n \cap Z) \cap (m \cap Z) \subseteq n \cap m$
31	28 29 30	mp2an	$⊢ (n \cap Z) \cap (m \cap Z) \subseteq n \cap m$
32		simp33	$⊢ ((J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \land (n \in J \land m \in J) \land (C \subseteq n \land D \subseteq m \land n \cap m = \emptyset)) \to n \cap m = \emptyset$
33	31 32	sseqtrid	$⊢ ((J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \land (n \in J \land m \in J) \land (C \subseteq n \land D \subseteq m \land n \cap m = \emptyset)) \to (n \cap Z) \cap (m \cap Z) \subseteq \emptyset$
34		ss0	$⊢ (n \cap Z) \cap (m \cap Z) \subseteq \emptyset \to (n \cap Z) \cap (m \cap Z) = \emptyset$
35	33 34	syl	$⊢ ((J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \land (n \in J \land m \in J) \land (C \subseteq n \land D \subseteq m \land n \cap m = \emptyset)) \to (n \cap Z) \cap (m \cap Z) = \emptyset$
36	23 27 35	3jca	$⊢ ((J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \land (n \in J \land m \in J) \land (C \subseteq n \land D \subseteq m \land n \cap m = \emptyset)) \to (C \subseteq n \cap Z \land D \subseteq m \cap Z \land (n \cap Z) \cap (m \cap Z) = \emptyset)$
37	13 16 36	3jca	$⊢ ((J \in Top \land (Z \in 𝒫 ⋃ J \land C \in Clsd (J ↾_{𝑡} Z) \land D \in Clsd (J ↾_{𝑡} Z)) \land C \cap D = \emptyset) \land (n \in J \land m \in J) \land (C \subseteq n \land D \subseteq m \land n \cap m = \emptyset)) \to (n \cap Z \in (J ↾_{𝑡} Z) \land m \cap Z \in (J ↾_{𝑡} Z) \land (C \subseteq n \cap Z \land D \subseteq m \cap Z \land (n \cap Z) \cap (m \cap Z) = \emptyset))$
38	4 8 37	iscnrm3lem7	$⊢ (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))$

Metamath Proof Explorer

Theorem iscnrm3llem2

Proof