This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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