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