seposep

Description: If two sets are separated by (open) neighborhoods, then they are separated subsets of the underlying set. Note that separatedness by open neighborhoods is equivalent to separatedness by neighborhoods. See sepnsepo . The relationship between separatedness and closure is also seen in isnrm , isnrm2 , isnrm3 . (Contributed by Zhi Wang, 7-Sep-2024)

	Ref	Expression
Hypotheses	sepdisj.1	$⊢ φ \to J \in Top$
	seposep.2	$⊢ φ \to \exists n \in J \exists m \in J (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset)$
Assertion	seposep	$⊢ φ \to ((S \subseteq ⋃ J \land T \subseteq ⋃ J) \land (S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset))$

Proof

Step	Hyp	Ref	Expression
1		sepdisj.1	$⊢ φ \to J \in Top$
2		seposep.2	$⊢ φ \to \exists n \in J \exists m \in J (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset)$
3		simp31	$⊢ (J \in Top \land (n \in J \land m \in J) \land (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset)) \to S \subseteq n$
4		simp1	$⊢ (J \in Top \land (n \in J \land m \in J) \land (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset)) \to J \in Top$
5		simp2l	$⊢ (J \in Top \land (n \in J \land m \in J) \land (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset)) \to n \in J$
6		eqid	$⊢ ⋃ J = ⋃ J$
7	6	eltopss	$⊢ (J \in Top \land n \in J) \to n \subseteq ⋃ J$
8	4 5 7	syl2anc	$⊢ (J \in Top \land (n \in J \land m \in J) \land (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset)) \to n \subseteq ⋃ J$
9	3 8	sstrd	$⊢ (J \in Top \land (n \in J \land m \in J) \land (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset)) \to S \subseteq ⋃ J$
10		simp32	$⊢ (J \in Top \land (n \in J \land m \in J) \land (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset)) \to T \subseteq m$
11		simp2r	$⊢ (J \in Top \land (n \in J \land m \in J) \land (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset)) \to m \in J$
12	6	eltopss	$⊢ (J \in Top \land m \in J) \to m \subseteq ⋃ J$
13	4 11 12	syl2anc	$⊢ (J \in Top \land (n \in J \land m \in J) \land (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset)) \to m \subseteq ⋃ J$
14	10 13	sstrd	$⊢ (J \in Top \land (n \in J \land m \in J) \land (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset)) \to T \subseteq ⋃ J$
15	6	opncld	$⊢ (J \in Top \land n \in J) \to ⋃ J ∖ n \in Clsd (J)$
16	4 5 15	syl2anc	$⊢ (J \in Top \land (n \in J \land m \in J) \land (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset)) \to ⋃ J ∖ n \in Clsd (J)$
17		incom	$⊢ n \cap m = m \cap n$
18		simp33	$⊢ (J \in Top \land (n \in J \land m \in J) \land (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset)) \to n \cap m = \emptyset$
19	17 18	eqtr3id	$⊢ (J \in Top \land (n \in J \land m \in J) \land (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset)) \to m \cap n = \emptyset$
20		reldisj	$⊢ m \subseteq ⋃ J \to (m \cap n = \emptyset \leftrightarrow m \subseteq ⋃ J ∖ n)$
21	20	biimpd	$⊢ m \subseteq ⋃ J \to (m \cap n = \emptyset \to m \subseteq ⋃ J ∖ n)$
22	13 19 21	sylc	$⊢ (J \in Top \land (n \in J \land m \in J) \land (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset)) \to m \subseteq ⋃ J ∖ n$
23	10 22	sstrd	$⊢ (J \in Top \land (n \in J \land m \in J) \land (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset)) \to T \subseteq ⋃ J ∖ n$
24	6	clsss2	$⊢ (⋃ J ∖ n \in Clsd (J) \land T \subseteq ⋃ J ∖ n) \to cls (J) (T) \subseteq ⋃ J ∖ n$
25	16 23 24	syl2anc	$⊢ (J \in Top \land (n \in J \land m \in J) \land (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset)) \to cls (J) (T) \subseteq ⋃ J ∖ n$
26	3	sscond	$⊢ (J \in Top \land (n \in J \land m \in J) \land (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset)) \to ⋃ J ∖ n \subseteq ⋃ J ∖ S$
27	25 26	sstrd	$⊢ (J \in Top \land (n \in J \land m \in J) \land (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset)) \to cls (J) (T) \subseteq ⋃ J ∖ S$
28		disjdif	$⊢ S \cap (⋃ J ∖ S) = \emptyset$
29	28	a1i	$⊢ (J \in Top \land (n \in J \land m \in J) \land (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset)) \to S \cap (⋃ J ∖ S) = \emptyset$
30	27 29	ssdisjdr	$⊢ (J \in Top \land (n \in J \land m \in J) \land (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset)) \to S \cap cls (J) (T) = \emptyset$
31	6	opncld	$⊢ (J \in Top \land m \in J) \to ⋃ J ∖ m \in Clsd (J)$
32	4 11 31	syl2anc	$⊢ (J \in Top \land (n \in J \land m \in J) \land (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset)) \to ⋃ J ∖ m \in Clsd (J)$
33		reldisj	$⊢ n \subseteq ⋃ J \to (n \cap m = \emptyset \leftrightarrow n \subseteq ⋃ J ∖ m)$
34	33	biimpd	$⊢ n \subseteq ⋃ J \to (n \cap m = \emptyset \to n \subseteq ⋃ J ∖ m)$
35	8 18 34	sylc	$⊢ (J \in Top \land (n \in J \land m \in J) \land (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset)) \to n \subseteq ⋃ J ∖ m$
36	3 35	sstrd	$⊢ (J \in Top \land (n \in J \land m \in J) \land (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset)) \to S \subseteq ⋃ J ∖ m$
37	6	clsss2	$⊢ (⋃ J ∖ m \in Clsd (J) \land S \subseteq ⋃ J ∖ m) \to cls (J) (S) \subseteq ⋃ J ∖ m$
38	32 36 37	syl2anc	$⊢ (J \in Top \land (n \in J \land m \in J) \land (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset)) \to cls (J) (S) \subseteq ⋃ J ∖ m$
39	10	sscond	$⊢ (J \in Top \land (n \in J \land m \in J) \land (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset)) \to ⋃ J ∖ m \subseteq ⋃ J ∖ T$
40	38 39	sstrd	$⊢ (J \in Top \land (n \in J \land m \in J) \land (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset)) \to cls (J) (S) \subseteq ⋃ J ∖ T$
41		disjdifr	$⊢ (⋃ J ∖ T) \cap T = \emptyset$
42	41	a1i	$⊢ (J \in Top \land (n \in J \land m \in J) \land (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset)) \to (⋃ J ∖ T) \cap T = \emptyset$
43	40 42	ssdisjd	$⊢ (J \in Top \land (n \in J \land m \in J) \land (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset)) \to cls (J) (S) \cap T = \emptyset$
44	30 43	jca	$⊢ (J \in Top \land (n \in J \land m \in J) \land (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset)) \to (S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset)$
45	9 14 44	jca31	$⊢ (J \in Top \land (n \in J \land m \in J) \land (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset)) \to ((S \subseteq ⋃ J \land T \subseteq ⋃ J) \land (S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset))$
46	45	3exp	$⊢ J \in Top \to ((n \in J \land m \in J) \to ((S \subseteq n \land T \subseteq m \land n \cap m = \emptyset) \to ((S \subseteq ⋃ J \land T \subseteq ⋃ J) \land (S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset))))$
47	46	rexlimdvv	$⊢ J \in Top \to (\exists n \in J \exists m \in J (S \subseteq n \land T \subseteq m \land n \cap m = \emptyset) \to ((S \subseteq ⋃ J \land T \subseteq ⋃ J) \land (S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset)))$
48	1 2 47	sylc	$⊢ φ \to ((S \subseteq ⋃ J \land T \subseteq ⋃ J) \land (S \cap cls (J) (T) = \emptyset \land cls (J) (S) \cap T = \emptyset))$

Metamath Proof Explorer

Theorem seposep

Proof