txcld

Description: The product of two closed sets is closed in the product topology. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 3-Sep-2015)

		Ref	Expression
	Assertion	txcld	$⊢ (A \in Clsd (R) \land B \in Clsd (S)) \to A \times B \in Clsd (R \times_{t} S)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ ⋃ R = ⋃ R$
2	1	cldss	$⊢ A \in Clsd (R) \to A \subseteq ⋃ R$
3		eqid	$⊢ ⋃ S = ⋃ S$
4	3	cldss	$⊢ B \in Clsd (S) \to B \subseteq ⋃ S$
5		xpss12	$⊢ (A \subseteq ⋃ R \land B \subseteq ⋃ S) \to A \times B \subseteq ⋃ R \times ⋃ S$
6	2 4 5	syl2an	$⊢ (A \in Clsd (R) \land B \in Clsd (S)) \to A \times B \subseteq ⋃ R \times ⋃ S$
7		cldrcl	$⊢ A \in Clsd (R) \to R \in Top$
8		cldrcl	$⊢ B \in Clsd (S) \to S \in Top$
9	1 3	txuni	$⊢ (R \in Top \land S \in Top) \to ⋃ R \times ⋃ S = ⋃ (R \times_{t} S)$
10	7 8 9	syl2an	$⊢ (A \in Clsd (R) \land B \in Clsd (S)) \to ⋃ R \times ⋃ S = ⋃ (R \times_{t} S)$
11	6 10	sseqtrd	$⊢ (A \in Clsd (R) \land B \in Clsd (S)) \to A \times B \subseteq ⋃ (R \times_{t} S)$
12		difxp	$⊢ (⋃ R \times ⋃ S) ∖ (A \times B) = ((⋃ R ∖ A) \times ⋃ S) \cup (⋃ R \times (⋃ S ∖ B))$
13	10	difeq1d	$⊢ (A \in Clsd (R) \land B \in Clsd (S)) \to (⋃ R \times ⋃ S) ∖ (A \times B) = ⋃ (R \times_{t} S) ∖ (A \times B)$
14	12 13	syl5eqr	$⊢ (A \in Clsd (R) \land B \in Clsd (S)) \to ((⋃ R ∖ A) \times ⋃ S) \cup (⋃ R \times (⋃ S ∖ B)) = ⋃ (R \times_{t} S) ∖ (A \times B)$
15		txtop	$⊢ (R \in Top \land S \in Top) \to R \times_{t} S \in Top$
16	7 8 15	syl2an	$⊢ (A \in Clsd (R) \land B \in Clsd (S)) \to R \times_{t} S \in Top$
17	7	adantr	$⊢ (A \in Clsd (R) \land B \in Clsd (S)) \to R \in Top$
18	8	adantl	$⊢ (A \in Clsd (R) \land B \in Clsd (S)) \to S \in Top$
19	1	cldopn	$⊢ A \in Clsd (R) \to ⋃ R ∖ A \in R$
20	19	adantr	$⊢ (A \in Clsd (R) \land B \in Clsd (S)) \to ⋃ R ∖ A \in R$
21	3	topopn	$⊢ S \in Top \to ⋃ S \in S$
22	18 21	syl	$⊢ (A \in Clsd (R) \land B \in Clsd (S)) \to ⋃ S \in S$
23		txopn	$⊢ ((R \in Top \land S \in Top) \land (⋃ R ∖ A \in R \land ⋃ S \in S)) \to (⋃ R ∖ A) \times ⋃ S \in (R \times_{t} S)$
24	17 18 20 22 23	syl22anc	$⊢ (A \in Clsd (R) \land B \in Clsd (S)) \to (⋃ R ∖ A) \times ⋃ S \in (R \times_{t} S)$
25	1	topopn	$⊢ R \in Top \to ⋃ R \in R$
26	17 25	syl	$⊢ (A \in Clsd (R) \land B \in Clsd (S)) \to ⋃ R \in R$
27	3	cldopn	$⊢ B \in Clsd (S) \to ⋃ S ∖ B \in S$
28	27	adantl	$⊢ (A \in Clsd (R) \land B \in Clsd (S)) \to ⋃ S ∖ B \in S$
29		txopn	$⊢ ((R \in Top \land S \in Top) \land (⋃ R \in R \land ⋃ S ∖ B \in S)) \to ⋃ R \times (⋃ S ∖ B) \in (R \times_{t} S)$
30	17 18 26 28 29	syl22anc	$⊢ (A \in Clsd (R) \land B \in Clsd (S)) \to ⋃ R \times (⋃ S ∖ B) \in (R \times_{t} S)$
31		unopn	$⊢ (R \times_{t} S \in Top \land (⋃ R ∖ A) \times ⋃ S \in (R \times_{t} S) \land ⋃ R \times (⋃ S ∖ B) \in (R \times_{t} S)) \to ((⋃ R ∖ A) \times ⋃ S) \cup (⋃ R \times (⋃ S ∖ B)) \in (R \times_{t} S)$
32	16 24 30 31	syl3anc	$⊢ (A \in Clsd (R) \land B \in Clsd (S)) \to ((⋃ R ∖ A) \times ⋃ S) \cup (⋃ R \times (⋃ S ∖ B)) \in (R \times_{t} S)$
33	14 32	eqeltrrd	$⊢ (A \in Clsd (R) \land B \in Clsd (S)) \to ⋃ (R \times_{t} S) ∖ (A \times B) \in (R \times_{t} S)$
34		eqid	$⊢ ⋃ (R \times_{t} S) = ⋃ (R \times_{t} S)$
35	34	iscld	$⊢ R \times_{t} S \in Top \to (A \times B \in Clsd (R \times_{t} S) \leftrightarrow (A \times B \subseteq ⋃ (R \times_{t} S) \land ⋃ (R \times_{t} S) ∖ (A \times B) \in (R \times_{t} S)))$
36	16 35	syl	$⊢ (A \in Clsd (R) \land B \in Clsd (S)) \to (A \times B \in Clsd (R \times_{t} S) \leftrightarrow (A \times B \subseteq ⋃ (R \times_{t} S) \land ⋃ (R \times_{t} S) ∖ (A \times B) \in (R \times_{t} S)))$
37	11 33 36	mpbir2and	$⊢ (A \in Clsd (R) \land B \in Clsd (S)) \to A \times B \in Clsd (R \times_{t} S)$

Metamath Proof Explorer

Theorem txcld

Proof