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