Metamath Proof Explorer


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 𝑆 ) ) )