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 A Clsd R B Clsd S A × B Clsd R × t S

Proof

Step Hyp Ref Expression
1 eqid R = R
2 1 cldss A Clsd R A R
3 eqid S = S
4 3 cldss B Clsd S B S
5 xpss12 A R B S A × B R × S
6 2 4 5 syl2an A Clsd R B Clsd S A × B R × S
7 cldrcl A Clsd R R Top
8 cldrcl B Clsd S S Top
9 1 3 txuni R Top S Top R × S = R × t S
10 7 8 9 syl2an A Clsd R B Clsd S R × S = R × t S
11 6 10 sseqtrd A Clsd R B Clsd S A × B R × t S
12 difxp R × S A × B = R A × S R × S B
13 10 difeq1d A Clsd R B Clsd S R × S A × B = R × t S A × B
14 12 13 eqtr3id A Clsd R B Clsd S R A × S R × S B = R × t S A × B
15 txtop R Top S Top R × t S Top
16 7 8 15 syl2an A Clsd R B Clsd S R × t S Top
17 7 adantr A Clsd R B Clsd S R Top
18 8 adantl A Clsd R B Clsd S S Top
19 1 cldopn A Clsd R R A R
20 19 adantr A Clsd R B Clsd S R A R
21 3 topopn S Top S S
22 18 21 syl A Clsd R B Clsd S S S
23 txopn R Top S Top R A R S S R A × S R × t S
24 17 18 20 22 23 syl22anc A Clsd R B Clsd S R A × S R × t S
25 1 topopn R Top R R
26 17 25 syl A Clsd R B Clsd S R R
27 3 cldopn B Clsd S S B S
28 27 adantl A Clsd R B Clsd S S B S
29 txopn R Top S Top R R S B S R × S B R × t S
30 17 18 26 28 29 syl22anc A Clsd R B Clsd S R × S B R × t S
31 unopn R × t S Top R A × S R × t S R × S B R × t S R A × S R × S B R × t S
32 16 24 30 31 syl3anc A Clsd R B Clsd S R A × S R × S B R × t S
33 14 32 eqeltrrd A Clsd R B Clsd S R × t S A × B R × t S
34 eqid R × t S = R × t S
35 34 iscld R × t S Top A × B Clsd R × t S A × B R × t S R × t S A × B R × t S
36 16 35 syl A Clsd R B Clsd S A × B Clsd R × t S A × B R × t S R × t S A × B R × t S
37 11 33 36 mpbir2and A Clsd R B Clsd S A × B Clsd R × t S