Theorem 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	⊢ ( ( 𝐴 ∈ ( Clsd ‘ 𝑅 ) ∧ 𝐵 ∈ ( Clsd ‘ 𝑆 ) ) → ( 𝐴 × 𝐵 ) ∈ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ∪ 𝑅 = ∪ 𝑅
2	1	cldss	⊢ ( 𝐴 ∈ ( Clsd ‘ 𝑅 ) → 𝐴 ⊆ ∪ 𝑅 )
3		eqid	⊢ ∪ 𝑆 = ∪ 𝑆
4	3	cldss	⊢ ( 𝐵 ∈ ( Clsd ‘ 𝑆 ) → 𝐵 ⊆ ∪ 𝑆 )
5		xpss12	⊢ ( ( 𝐴 ⊆ ∪ 𝑅 ∧ 𝐵 ⊆ ∪ 𝑆 ) → ( 𝐴 × 𝐵 ) ⊆ ( ∪ 𝑅 × ∪ 𝑆 ) )
6	2 4 5	syl2an	⊢ ( ( 𝐴 ∈ ( Clsd ‘ 𝑅 ) ∧ 𝐵 ∈ ( Clsd ‘ 𝑆 ) ) → ( 𝐴 × 𝐵 ) ⊆ ( ∪ 𝑅 × ∪ 𝑆 ) )
7		cldrcl	⊢ ( 𝐴 ∈ ( Clsd ‘ 𝑅 ) → 𝑅 ∈ Top )
8		cldrcl	⊢ ( 𝐵 ∈ ( Clsd ‘ 𝑆 ) → 𝑆 ∈ Top )
9	1 3	txuni	⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( ∪ 𝑅 × ∪ 𝑆 ) = ∪ ( 𝑅 ×t 𝑆 ) )
10	7 8 9	syl2an	⊢ ( ( 𝐴 ∈ ( Clsd ‘ 𝑅 ) ∧ 𝐵 ∈ ( Clsd ‘ 𝑆 ) ) → ( ∪ 𝑅 × ∪ 𝑆 ) = ∪ ( 𝑅 ×t 𝑆 ) )
11	6 10	sseqtrd	⊢ ( ( 𝐴 ∈ ( Clsd ‘ 𝑅 ) ∧ 𝐵 ∈ ( Clsd ‘ 𝑆 ) ) → ( 𝐴 × 𝐵 ) ⊆ ∪ ( 𝑅 ×t 𝑆 ) )
12		difxp	⊢ ( ( ∪ 𝑅 × ∪ 𝑆 ) ∖ ( 𝐴 × 𝐵 ) ) = ( ( ( ∪ 𝑅 ∖ 𝐴 ) × ∪ 𝑆 ) ∪ ( ∪ 𝑅 × ( ∪ 𝑆 ∖ 𝐵 ) ) )
13	10	difeq1d	⊢ ( ( 𝐴 ∈ ( Clsd ‘ 𝑅 ) ∧ 𝐵 ∈ ( Clsd ‘ 𝑆 ) ) → ( ( ∪ 𝑅 × ∪ 𝑆 ) ∖ ( 𝐴 × 𝐵 ) ) = ( ∪ ( 𝑅 ×t 𝑆 ) ∖ ( 𝐴 × 𝐵 ) ) )
14	12 13	eqtr3id	⊢ ( ( 𝐴 ∈ ( Clsd ‘ 𝑅 ) ∧ 𝐵 ∈ ( Clsd ‘ 𝑆 ) ) → ( ( ( ∪ 𝑅 ∖ 𝐴 ) × ∪ 𝑆 ) ∪ ( ∪ 𝑅 × ( ∪ 𝑆 ∖ 𝐵 ) ) ) = ( ∪ ( 𝑅 ×t 𝑆 ) ∖ ( 𝐴 × 𝐵 ) ) )
15		txtop	⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 ×t 𝑆 ) ∈ Top )
16	7 8 15	syl2an	⊢ ( ( 𝐴 ∈ ( Clsd ‘ 𝑅 ) ∧ 𝐵 ∈ ( Clsd ‘ 𝑆 ) ) → ( 𝑅 ×t 𝑆 ) ∈ Top )
17	7	adantr	⊢ ( ( 𝐴 ∈ ( Clsd ‘ 𝑅 ) ∧ 𝐵 ∈ ( Clsd ‘ 𝑆 ) ) → 𝑅 ∈ Top )
18	8	adantl	⊢ ( ( 𝐴 ∈ ( Clsd ‘ 𝑅 ) ∧ 𝐵 ∈ ( Clsd ‘ 𝑆 ) ) → 𝑆 ∈ Top )
19	1	cldopn	⊢ ( 𝐴 ∈ ( Clsd ‘ 𝑅 ) → ( ∪ 𝑅 ∖ 𝐴 ) ∈ 𝑅 )
20	19	adantr	⊢ ( ( 𝐴 ∈ ( Clsd ‘ 𝑅 ) ∧ 𝐵 ∈ ( Clsd ‘ 𝑆 ) ) → ( ∪ 𝑅 ∖ 𝐴 ) ∈ 𝑅 )
21	3	topopn	⊢ ( 𝑆 ∈ Top → ∪ 𝑆 ∈ 𝑆 )
22	18 21	syl	⊢ ( ( 𝐴 ∈ ( Clsd ‘ 𝑅 ) ∧ 𝐵 ∈ ( Clsd ‘ 𝑆 ) ) → ∪ 𝑆 ∈ 𝑆 )
23		txopn	⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( ( ∪ 𝑅 ∖ 𝐴 ) ∈ 𝑅 ∧ ∪ 𝑆 ∈ 𝑆 ) ) → ( ( ∪ 𝑅 ∖ 𝐴 ) × ∪ 𝑆 ) ∈ ( 𝑅 ×t 𝑆 ) )
24	17 18 20 22 23	syl22anc	⊢ ( ( 𝐴 ∈ ( Clsd ‘ 𝑅 ) ∧ 𝐵 ∈ ( Clsd ‘ 𝑆 ) ) → ( ( ∪ 𝑅 ∖ 𝐴 ) × ∪ 𝑆 ) ∈ ( 𝑅 ×t 𝑆 ) )
25	1	topopn	⊢ ( 𝑅 ∈ Top → ∪ 𝑅 ∈ 𝑅 )
26	17 25	syl	⊢ ( ( 𝐴 ∈ ( Clsd ‘ 𝑅 ) ∧ 𝐵 ∈ ( Clsd ‘ 𝑆 ) ) → ∪ 𝑅 ∈ 𝑅 )
27	3	cldopn	⊢ ( 𝐵 ∈ ( Clsd ‘ 𝑆 ) → ( ∪ 𝑆 ∖ 𝐵 ) ∈ 𝑆 )
28	27	adantl	⊢ ( ( 𝐴 ∈ ( Clsd ‘ 𝑅 ) ∧ 𝐵 ∈ ( Clsd ‘ 𝑆 ) ) → ( ∪ 𝑆 ∖ 𝐵 ) ∈ 𝑆 )
29		txopn	⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( ∪ 𝑅 ∈ 𝑅 ∧ ( ∪ 𝑆 ∖ 𝐵 ) ∈ 𝑆 ) ) → ( ∪ 𝑅 × ( ∪ 𝑆 ∖ 𝐵 ) ) ∈ ( 𝑅 ×t 𝑆 ) )
30	17 18 26 28 29	syl22anc	⊢ ( ( 𝐴 ∈ ( Clsd ‘ 𝑅 ) ∧ 𝐵 ∈ ( Clsd ‘ 𝑆 ) ) → ( ∪ 𝑅 × ( ∪ 𝑆 ∖ 𝐵 ) ) ∈ ( 𝑅 ×t 𝑆 ) )
31		unopn	⊢ ( ( ( 𝑅 ×t 𝑆 ) ∈ Top ∧ ( ( ∪ 𝑅 ∖ 𝐴 ) × ∪ 𝑆 ) ∈ ( 𝑅 ×t 𝑆 ) ∧ ( ∪ 𝑅 × ( ∪ 𝑆 ∖ 𝐵 ) ) ∈ ( 𝑅 ×t 𝑆 ) ) → ( ( ( ∪ 𝑅 ∖ 𝐴 ) × ∪ 𝑆 ) ∪ ( ∪ 𝑅 × ( ∪ 𝑆 ∖ 𝐵 ) ) ) ∈ ( 𝑅 ×t 𝑆 ) )
32	16 24 30 31	syl3anc	⊢ ( ( 𝐴 ∈ ( Clsd ‘ 𝑅 ) ∧ 𝐵 ∈ ( Clsd ‘ 𝑆 ) ) → ( ( ( ∪ 𝑅 ∖ 𝐴 ) × ∪ 𝑆 ) ∪ ( ∪ 𝑅 × ( ∪ 𝑆 ∖ 𝐵 ) ) ) ∈ ( 𝑅 ×t 𝑆 ) )
33	14 32	eqeltrrd	⊢ ( ( 𝐴 ∈ ( Clsd ‘ 𝑅 ) ∧ 𝐵 ∈ ( Clsd ‘ 𝑆 ) ) → ( ∪ ( 𝑅 ×t 𝑆 ) ∖ ( 𝐴 × 𝐵 ) ) ∈ ( 𝑅 ×t 𝑆 ) )
34		eqid	⊢ ∪ ( 𝑅 ×t 𝑆 ) = ∪ ( 𝑅 ×t 𝑆 )
35	34	iscld	⊢ ( ( 𝑅 ×t 𝑆 ) ∈ Top → ( ( 𝐴 × 𝐵 ) ∈ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ↔ ( ( 𝐴 × 𝐵 ) ⊆ ∪ ( 𝑅 ×t 𝑆 ) ∧ ( ∪ ( 𝑅 ×t 𝑆 ) ∖ ( 𝐴 × 𝐵 ) ) ∈ ( 𝑅 ×t 𝑆 ) ) ) )
36	16 35	syl	⊢ ( ( 𝐴 ∈ ( Clsd ‘ 𝑅 ) ∧ 𝐵 ∈ ( Clsd ‘ 𝑆 ) ) → ( ( 𝐴 × 𝐵 ) ∈ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ↔ ( ( 𝐴 × 𝐵 ) ⊆ ∪ ( 𝑅 ×t 𝑆 ) ∧ ( ∪ ( 𝑅 ×t 𝑆 ) ∖ ( 𝐴 × 𝐵 ) ) ∈ ( 𝑅 ×t 𝑆 ) ) ) )
37	11 33 36	mpbir2and	⊢ ( ( 𝐴 ∈ ( Clsd ‘ 𝑅 ) ∧ 𝐵 ∈ ( Clsd ‘ 𝑆 ) ) → ( 𝐴 × 𝐵 ) ∈ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) )