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 AClsdRBClsdSA×BClsdR×tS

Proof

Step Hyp Ref Expression
1 eqid R=R
2 1 cldss AClsdRAR
3 eqid S=S
4 3 cldss BClsdSBS
5 xpss12 ARBSA×BR×S
6 2 4 5 syl2an AClsdRBClsdSA×BR×S
7 cldrcl AClsdRRTop
8 cldrcl BClsdSSTop
9 1 3 txuni RTopSTopR×S=R×tS
10 7 8 9 syl2an AClsdRBClsdSR×S=R×tS
11 6 10 sseqtrd AClsdRBClsdSA×BR×tS
12 difxp R×SA×B=RA×SR×SB
13 10 difeq1d AClsdRBClsdSR×SA×B=R×tSA×B
14 12 13 eqtr3id AClsdRBClsdSRA×SR×SB=R×tSA×B
15 txtop RTopSTopR×tSTop
16 7 8 15 syl2an AClsdRBClsdSR×tSTop
17 7 adantr AClsdRBClsdSRTop
18 8 adantl AClsdRBClsdSSTop
19 1 cldopn AClsdRRAR
20 19 adantr AClsdRBClsdSRAR
21 3 topopn STopSS
22 18 21 syl AClsdRBClsdSSS
23 txopn RTopSTopRARSSRA×SR×tS
24 17 18 20 22 23 syl22anc AClsdRBClsdSRA×SR×tS
25 1 topopn RTopRR
26 17 25 syl AClsdRBClsdSRR
27 3 cldopn BClsdSSBS
28 27 adantl AClsdRBClsdSSBS
29 txopn RTopSTopRRSBSR×SBR×tS
30 17 18 26 28 29 syl22anc AClsdRBClsdSR×SBR×tS
31 unopn R×tSTopRA×SR×tSR×SBR×tSRA×SR×SBR×tS
32 16 24 30 31 syl3anc AClsdRBClsdSRA×SR×SBR×tS
33 14 32 eqeltrrd AClsdRBClsdSR×tSA×BR×tS
34 eqid R×tS=R×tS
35 34 iscld R×tSTopA×BClsdR×tSA×BR×tSR×tSA×BR×tS
36 16 35 syl AClsdRBClsdSA×BClsdR×tSA×BR×tSR×tSA×BR×tS
37 11 33 36 mpbir2and AClsdRBClsdSA×BClsdR×tS