iscnrm3rlem8

Description: Lemma for iscnrm3r . Disjoint open neighborhoods in the subspace topology are disjoint open neighborhoods in the original topology given that the subspace is an open set in the original topology. Therefore, given any two sets separated in the original topology and separated by open neighborhoods in the subspace topology, they must be separated by open neighborhoods in the original topology. (Contributed by Zhi Wang, 5-Sep-2024)

		Ref	Expression
	Assertion	iscnrm3rlem8	$⊢ (J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J) \land (S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset)) \to (\exists l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \exists k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) (cls (J) (S) ∖ cls (J) (T) \subseteq l \land cls (J) (T) ∖ cls (J) (S) \subseteq k \land l \cap k = \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		sseq2	$⊢ n = l \to (S \subseteq n \leftrightarrow S \subseteq l)$
2		ineq1	$⊢ n = l \to n \cap m = l \cap m$
3	2	eqeq1d	$⊢ n = l \to (n \cap m = \emptyset \leftrightarrow l \cap m = \emptyset)$
4	1 3	3anbi13d	$⊢ n = l \to ((S \subseteq n \land T \subseteq m \land n \cap m = \emptyset) \leftrightarrow (S \subseteq l \land T \subseteq m \land l \cap m = \emptyset))$
5		sseq2	$⊢ m = k \to (T \subseteq m \leftrightarrow T \subseteq k)$
6		ineq2	$⊢ m = k \to l \cap m = l \cap k$
7	6	eqeq1d	$⊢ m = k \to (l \cap m = \emptyset \leftrightarrow l \cap k = \emptyset)$
8	5 7	3anbi23d	$⊢ m = k \to ((S \subseteq l \land T \subseteq m \land l \cap m = \emptyset) \leftrightarrow (S \subseteq l \land T \subseteq k \land l \cap k = \emptyset))$
9		simp11	$⊢ ((J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J) \land (S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset)) \land (l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \land k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T))))) \land (cls (J) (S) ∖ cls (J) (T) \subseteq l \land cls (J) (T) ∖ cls (J) (S) \subseteq k \land l \cap k = \emptyset)) \to J \in Top$
10		simp12l	$⊢ ((J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J) \land (S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset)) \land (l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \land k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T))))) \land (cls (J) (S) ∖ cls (J) (T) \subseteq l \land cls (J) (T) ∖ cls (J) (S) \subseteq k \land l \cap k = \emptyset)) \to S \in 𝒫 ⋃ J$
11	10	elpwid	$⊢ ((J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J) \land (S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset)) \land (l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \land k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T))))) \land (cls (J) (S) ∖ cls (J) (T) \subseteq l \land cls (J) (T) ∖ cls (J) (S) \subseteq k \land l \cap k = \emptyset)) \to S \subseteq ⋃ J$
12		simp12r	$⊢ ((J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J) \land (S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset)) \land (l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \land k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T))))) \land (cls (J) (S) ∖ cls (J) (T) \subseteq l \land cls (J) (T) ∖ cls (J) (S) \subseteq k \land l \cap k = \emptyset)) \to T \in 𝒫 ⋃ J$
13	12	elpwid	$⊢ ((J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J) \land (S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset)) \land (l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \land k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T))))) \land (cls (J) (S) ∖ cls (J) (T) \subseteq l \land cls (J) (T) ∖ cls (J) (S) \subseteq k \land l \cap k = \emptyset)) \to T \subseteq ⋃ J$
14		simp2l	$⊢ ((J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J) \land (S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset)) \land (l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \land k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T))))) \land (cls (J) (S) ∖ cls (J) (T) \subseteq l \land cls (J) (T) ∖ cls (J) (S) \subseteq k \land l \cap k = \emptyset)) \to l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T))))$
15	9 11 13 14	iscnrm3rlem7	$⊢ ((J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J) \land (S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset)) \land (l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \land k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T))))) \land (cls (J) (S) ∖ cls (J) (T) \subseteq l \land cls (J) (T) ∖ cls (J) (S) \subseteq k \land l \cap k = \emptyset)) \to l \in J$
16		simp2r	$⊢ ((J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J) \land (S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset)) \land (l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \land k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T))))) \land (cls (J) (S) ∖ cls (J) (T) \subseteq l \land cls (J) (T) ∖ cls (J) (S) \subseteq k \land l \cap k = \emptyset)) \to k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T))))$
17	9 11 13 16	iscnrm3rlem7	$⊢ ((J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J) \land (S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset)) \land (l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \land k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T))))) \land (cls (J) (S) ∖ cls (J) (T) \subseteq l \land cls (J) (T) ∖ cls (J) (S) \subseteq k \land l \cap k = \emptyset)) \to k \in J$
18		simp13l	$⊢ ((J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J) \land (S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset)) \land (l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \land k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T))))) \land (cls (J) (S) ∖ cls (J) (T) \subseteq l \land cls (J) (T) ∖ cls (J) (S) \subseteq k \land l \cap k = \emptyset)) \to S \cap cls (J) (T) = \emptyset$
19		simp31	$⊢ ((J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J) \land (S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset)) \land (l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \land k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T))))) \land (cls (J) (S) ∖ cls (J) (T) \subseteq l \land cls (J) (T) ∖ cls (J) (S) \subseteq k \land l \cap k = \emptyset)) \to cls (J) (S) ∖ cls (J) (T) \subseteq l$
20	9 11 18 19	iscnrm3rlem4	$⊢ ((J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J) \land (S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset)) \land (l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \land k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T))))) \land (cls (J) (S) ∖ cls (J) (T) \subseteq l \land cls (J) (T) ∖ cls (J) (S) \subseteq k \land l \cap k = \emptyset)) \to S \subseteq l$
21		incom	$⊢ cls (J) (S) \cap T = T \cap cls (J) (S)$
22		simp13r	$⊢ ((J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J) \land (S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset)) \land (l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \land k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T))))) \land (cls (J) (S) ∖ cls (J) (T) \subseteq l \land cls (J) (T) ∖ cls (J) (S) \subseteq k \land l \cap k = \emptyset)) \to cls (J) (S) \cap T = \emptyset$
23	21 22	eqtr3id	$⊢ ((J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J) \land (S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset)) \land (l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \land k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T))))) \land (cls (J) (S) ∖ cls (J) (T) \subseteq l \land cls (J) (T) ∖ cls (J) (S) \subseteq k \land l \cap k = \emptyset)) \to T \cap cls (J) (S) = \emptyset$
24		simp32	$⊢ ((J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J) \land (S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset)) \land (l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \land k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T))))) \land (cls (J) (S) ∖ cls (J) (T) \subseteq l \land cls (J) (T) ∖ cls (J) (S) \subseteq k \land l \cap k = \emptyset)) \to cls (J) (T) ∖ cls (J) (S) \subseteq k$
25	9 13 23 24	iscnrm3rlem4	$⊢ ((J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J) \land (S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset)) \land (l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \land k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T))))) \land (cls (J) (S) ∖ cls (J) (T) \subseteq l \land cls (J) (T) ∖ cls (J) (S) \subseteq k \land l \cap k = \emptyset)) \to T \subseteq k$
26		simp33	$⊢ ((J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J) \land (S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset)) \land (l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \land k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T))))) \land (cls (J) (S) ∖ cls (J) (T) \subseteq l \land cls (J) (T) ∖ cls (J) (S) \subseteq k \land l \cap k = \emptyset)) \to l \cap k = \emptyset$
27	20 25 26	3jca	$⊢ ((J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J) \land (S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset)) \land (l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \land k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T))))) \land (cls (J) (S) ∖ cls (J) (T) \subseteq l \land cls (J) (T) ∖ cls (J) (S) \subseteq k \land l \cap k = \emptyset)) \to (S \subseteq l \land T \subseteq k \land l \cap k = \emptyset)$
28	15 17 27	3jca	$⊢ ((J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J) \land (S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset)) \land (l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \land k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T))))) \land (cls (J) (S) ∖ cls (J) (T) \subseteq l \land cls (J) (T) ∖ cls (J) (S) \subseteq k \land l \cap k = \emptyset)) \to (l \in J \land k \in J \land (S \subseteq l \land T \subseteq k \land l \cap k = \emptyset))$
29	4 8 28	iscnrm3lem7	$⊢ (J \in Top \land (S \in 𝒫 ⋃ J \land T \in 𝒫 ⋃ J) \land (S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset)) \to (\exists l \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) \exists k \in (J ↾_{𝑡} (⋃ J ∖ (cls (J) (S) \cap cls (J) (T)))) (cls (J) (S) ∖ cls (J) (T) \subseteq l \land cls (J) (T) ∖ cls (J) (S) \subseteq k \land l \cap k = \emptyset) \to \exists n \in J \exists m \in J (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset))$

Metamath Proof Explorer

Theorem iscnrm3rlem8

Proof