clsun

Description: A pairwise union of closures is the closure of the union. (Contributed by Jeff Hankins, 31-Aug-2009)

		Ref	Expression
	Hypothesis	clsun.1	$⊢ X = ⋃ J$
	Assertion	clsun	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to cls (J) (A \cup B) = cls (J) (A) \cup cls (J) (B)$

Proof

Step	Hyp	Ref	Expression
1		clsun.1	$⊢ X = ⋃ J$
2		difundi	$⊢ X ∖ (A \cup B) = (X ∖ A) \cap (X ∖ B)$
3	2	fveq2i	$⊢ int (J) (X ∖ (A \cup B)) = int (J) ((X ∖ A) \cap (X ∖ B))$
4		difss	$⊢ X ∖ A \subseteq X$
5		difss	$⊢ X ∖ B \subseteq X$
6	1	ntrin	$⊢ (J \in Top \land X ∖ A \subseteq X \land X ∖ B \subseteq X) \to int (J) ((X ∖ A) \cap (X ∖ B)) = int (J) (X ∖ A) \cap int (J) (X ∖ B)$
7	4 5 6	mp3an23	$⊢ J \in Top \to int (J) ((X ∖ A) \cap (X ∖ B)) = int (J) (X ∖ A) \cap int (J) (X ∖ B)$
8	7	3ad2ant1	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to int (J) ((X ∖ A) \cap (X ∖ B)) = int (J) (X ∖ A) \cap int (J) (X ∖ B)$
9	3 8	eqtrid	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to int (J) (X ∖ (A \cup B)) = int (J) (X ∖ A) \cap int (J) (X ∖ B)$
10		simp1	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to J \in Top$
11		unss	$⊢ (A \subseteq X \land B \subseteq X) \leftrightarrow A \cup B \subseteq X$
12	11	biimpi	$⊢ (A \subseteq X \land B \subseteq X) \to A \cup B \subseteq X$
13	12	3adant1	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to A \cup B \subseteq X$
14	1	ntrdif	$⊢ (J \in Top \land A \cup B \subseteq X) \to int (J) (X ∖ (A \cup B)) = X ∖ cls (J) (A \cup B)$
15	10 13 14	syl2anc	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to int (J) (X ∖ (A \cup B)) = X ∖ cls (J) (A \cup B)$
16	1	ntrdif	$⊢ (J \in Top \land A \subseteq X) \to int (J) (X ∖ A) = X ∖ cls (J) (A)$
17	16	3adant3	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to int (J) (X ∖ A) = X ∖ cls (J) (A)$
18	1	ntrdif	$⊢ (J \in Top \land B \subseteq X) \to int (J) (X ∖ B) = X ∖ cls (J) (B)$
19	18	3adant2	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to int (J) (X ∖ B) = X ∖ cls (J) (B)$
20	17 19	ineq12d	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to int (J) (X ∖ A) \cap int (J) (X ∖ B) = (X ∖ cls (J) (A)) \cap (X ∖ cls (J) (B))$
21		difundi	$⊢ X ∖ (cls (J) (A) \cup cls (J) (B)) = (X ∖ cls (J) (A)) \cap (X ∖ cls (J) (B))$
22	20 21	eqtr4di	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to int (J) (X ∖ A) \cap int (J) (X ∖ B) = X ∖ (cls (J) (A) \cup cls (J) (B))$
23	9 15 22	3eqtr3d	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to X ∖ cls (J) (A \cup B) = X ∖ (cls (J) (A) \cup cls (J) (B))$
24	23	difeq2d	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to X ∖ (X ∖ cls (J) (A \cup B)) = X ∖ (X ∖ (cls (J) (A) \cup cls (J) (B)))$
25	1	clscld	$⊢ (J \in Top \land A \cup B \subseteq X) \to cls (J) (A \cup B) \in Clsd (J)$
26	10 13 25	syl2anc	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to cls (J) (A \cup B) \in Clsd (J)$
27	1	cldss	$⊢ cls (J) (A \cup B) \in Clsd (J) \to cls (J) (A \cup B) \subseteq X$
28	26 27	syl	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to cls (J) (A \cup B) \subseteq X$
29		dfss4	$⊢ cls (J) (A \cup B) \subseteq X \leftrightarrow X ∖ (X ∖ cls (J) (A \cup B)) = cls (J) (A \cup B)$
30	28 29	sylib	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to X ∖ (X ∖ cls (J) (A \cup B)) = cls (J) (A \cup B)$
31	1	clsss3	$⊢ (J \in Top \land A \subseteq X) \to cls (J) (A) \subseteq X$
32	31	3adant3	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to cls (J) (A) \subseteq X$
33	1	clsss3	$⊢ (J \in Top \land B \subseteq X) \to cls (J) (B) \subseteq X$
34	33	3adant2	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to cls (J) (B) \subseteq X$
35	32 34	jca	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to (cls (J) (A) \subseteq X \land cls (J) (B) \subseteq X)$
36		unss	$⊢ (cls (J) (A) \subseteq X \land cls (J) (B) \subseteq X) \leftrightarrow cls (J) (A) \cup cls (J) (B) \subseteq X$
37		dfss4	$⊢ cls (J) (A) \cup cls (J) (B) \subseteq X \leftrightarrow X ∖ (X ∖ (cls (J) (A) \cup cls (J) (B))) = cls (J) (A) \cup cls (J) (B)$
38	36 37	bitri	$⊢ (cls (J) (A) \subseteq X \land cls (J) (B) \subseteq X) \leftrightarrow X ∖ (X ∖ (cls (J) (A) \cup cls (J) (B))) = cls (J) (A) \cup cls (J) (B)$
39	35 38	sylib	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to X ∖ (X ∖ (cls (J) (A) \cup cls (J) (B))) = cls (J) (A) \cup cls (J) (B)$
40	24 30 39	3eqtr3d	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to cls (J) (A \cup B) = cls (J) (A) \cup cls (J) (B)$

Metamath Proof Explorer

Theorem clsun

Proof