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 e. ( Clsd ` R ) /\ B e. ( Clsd ` S ) ) -> ( A X. B ) e. ( Clsd ` ( R tX S ) ) )

Proof

Step Hyp Ref Expression
1 eqid
 |-  U. R = U. R
2 1 cldss
 |-  ( A e. ( Clsd ` R ) -> A C_ U. R )
3 eqid
 |-  U. S = U. S
4 3 cldss
 |-  ( B e. ( Clsd ` S ) -> B C_ U. S )
5 xpss12
 |-  ( ( A C_ U. R /\ B C_ U. S ) -> ( A X. B ) C_ ( U. R X. U. S ) )
6 2 4 5 syl2an
 |-  ( ( A e. ( Clsd ` R ) /\ B e. ( Clsd ` S ) ) -> ( A X. B ) C_ ( U. R X. U. S ) )
7 cldrcl
 |-  ( A e. ( Clsd ` R ) -> R e. Top )
8 cldrcl
 |-  ( B e. ( Clsd ` S ) -> S e. Top )
9 1 3 txuni
 |-  ( ( R e. Top /\ S e. Top ) -> ( U. R X. U. S ) = U. ( R tX S ) )
10 7 8 9 syl2an
 |-  ( ( A e. ( Clsd ` R ) /\ B e. ( Clsd ` S ) ) -> ( U. R X. U. S ) = U. ( R tX S ) )
11 6 10 sseqtrd
 |-  ( ( A e. ( Clsd ` R ) /\ B e. ( Clsd ` S ) ) -> ( A X. B ) C_ U. ( R tX S ) )
12 difxp
 |-  ( ( U. R X. U. S ) \ ( A X. B ) ) = ( ( ( U. R \ A ) X. U. S ) u. ( U. R X. ( U. S \ B ) ) )
13 10 difeq1d
 |-  ( ( A e. ( Clsd ` R ) /\ B e. ( Clsd ` S ) ) -> ( ( U. R X. U. S ) \ ( A X. B ) ) = ( U. ( R tX S ) \ ( A X. B ) ) )
14 12 13 eqtr3id
 |-  ( ( A e. ( Clsd ` R ) /\ B e. ( Clsd ` S ) ) -> ( ( ( U. R \ A ) X. U. S ) u. ( U. R X. ( U. S \ B ) ) ) = ( U. ( R tX S ) \ ( A X. B ) ) )
15 txtop
 |-  ( ( R e. Top /\ S e. Top ) -> ( R tX S ) e. Top )
16 7 8 15 syl2an
 |-  ( ( A e. ( Clsd ` R ) /\ B e. ( Clsd ` S ) ) -> ( R tX S ) e. Top )
17 7 adantr
 |-  ( ( A e. ( Clsd ` R ) /\ B e. ( Clsd ` S ) ) -> R e. Top )
18 8 adantl
 |-  ( ( A e. ( Clsd ` R ) /\ B e. ( Clsd ` S ) ) -> S e. Top )
19 1 cldopn
 |-  ( A e. ( Clsd ` R ) -> ( U. R \ A ) e. R )
20 19 adantr
 |-  ( ( A e. ( Clsd ` R ) /\ B e. ( Clsd ` S ) ) -> ( U. R \ A ) e. R )
21 3 topopn
 |-  ( S e. Top -> U. S e. S )
22 18 21 syl
 |-  ( ( A e. ( Clsd ` R ) /\ B e. ( Clsd ` S ) ) -> U. S e. S )
23 txopn
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( ( U. R \ A ) e. R /\ U. S e. S ) ) -> ( ( U. R \ A ) X. U. S ) e. ( R tX S ) )
24 17 18 20 22 23 syl22anc
 |-  ( ( A e. ( Clsd ` R ) /\ B e. ( Clsd ` S ) ) -> ( ( U. R \ A ) X. U. S ) e. ( R tX S ) )
25 1 topopn
 |-  ( R e. Top -> U. R e. R )
26 17 25 syl
 |-  ( ( A e. ( Clsd ` R ) /\ B e. ( Clsd ` S ) ) -> U. R e. R )
27 3 cldopn
 |-  ( B e. ( Clsd ` S ) -> ( U. S \ B ) e. S )
28 27 adantl
 |-  ( ( A e. ( Clsd ` R ) /\ B e. ( Clsd ` S ) ) -> ( U. S \ B ) e. S )
29 txopn
 |-  ( ( ( R e. Top /\ S e. Top ) /\ ( U. R e. R /\ ( U. S \ B ) e. S ) ) -> ( U. R X. ( U. S \ B ) ) e. ( R tX S ) )
30 17 18 26 28 29 syl22anc
 |-  ( ( A e. ( Clsd ` R ) /\ B e. ( Clsd ` S ) ) -> ( U. R X. ( U. S \ B ) ) e. ( R tX S ) )
31 unopn
 |-  ( ( ( R tX S ) e. Top /\ ( ( U. R \ A ) X. U. S ) e. ( R tX S ) /\ ( U. R X. ( U. S \ B ) ) e. ( R tX S ) ) -> ( ( ( U. R \ A ) X. U. S ) u. ( U. R X. ( U. S \ B ) ) ) e. ( R tX S ) )
32 16 24 30 31 syl3anc
 |-  ( ( A e. ( Clsd ` R ) /\ B e. ( Clsd ` S ) ) -> ( ( ( U. R \ A ) X. U. S ) u. ( U. R X. ( U. S \ B ) ) ) e. ( R tX S ) )
33 14 32 eqeltrrd
 |-  ( ( A e. ( Clsd ` R ) /\ B e. ( Clsd ` S ) ) -> ( U. ( R tX S ) \ ( A X. B ) ) e. ( R tX S ) )
34 eqid
 |-  U. ( R tX S ) = U. ( R tX S )
35 34 iscld
 |-  ( ( R tX S ) e. Top -> ( ( A X. B ) e. ( Clsd ` ( R tX S ) ) <-> ( ( A X. B ) C_ U. ( R tX S ) /\ ( U. ( R tX S ) \ ( A X. B ) ) e. ( R tX S ) ) ) )
36 16 35 syl
 |-  ( ( A e. ( Clsd ` R ) /\ B e. ( Clsd ` S ) ) -> ( ( A X. B ) e. ( Clsd ` ( R tX S ) ) <-> ( ( A X. B ) C_ U. ( R tX S ) /\ ( U. ( R tX S ) \ ( A X. B ) ) e. ( R tX S ) ) ) )
37 11 33 36 mpbir2and
 |-  ( ( A e. ( Clsd ` R ) /\ B e. ( Clsd ` S ) ) -> ( A X. B ) e. ( Clsd ` ( R tX S ) ) )