Metamath Proof Explorer

Theorem txopn

Description: The product of two open sets is open in the product topology. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion txopn 
|- ( ( ( R e. V /\ S e. W ) /\ ( A e. R /\ B e. S ) ) -> ( A X. B ) e. ( R tX S ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ran ( u e. R , v e. S |-> ( u X. v ) ) = ran ( u e. R , v e. S |-> ( u X. v ) )
2 1 txbasex 
 |-  ( ( R e. V /\ S e. W ) -> ran ( u e. R , v e. S |-> ( u X. v ) ) e. _V )
3 bastg 
 |-  ( ran ( u e. R , v e. S |-> ( u X. v ) ) e. _V -> ran ( u e. R , v e. S |-> ( u X. v ) ) C_ ( topGen ` ran ( u e. R , v e. S |-> ( u X. v ) ) ) )
4 2 3 syl 
 |-  ( ( R e. V /\ S e. W ) -> ran ( u e. R , v e. S |-> ( u X. v ) ) C_ ( topGen ` ran ( u e. R , v e. S |-> ( u X. v ) ) ) )
5 4 adantr 
 |-  ( ( ( R e. V /\ S e. W ) /\ ( A e. R /\ B e. S ) ) -> ran ( u e. R , v e. S |-> ( u X. v ) ) C_ ( topGen ` ran ( u e. R , v e. S |-> ( u X. v ) ) ) )
6 eqid 
 |-  ( A X. B ) = ( A X. B )
7 xpeq1 
 |-  ( u = A -> ( u X. v ) = ( A X. v ) )
8 7 eqeq2d 
 |-  ( u = A -> ( ( A X. B ) = ( u X. v ) <-> ( A X. B ) = ( A X. v ) ) )
9 xpeq2 
 |-  ( v = B -> ( A X. v ) = ( A X. B ) )
10 9 eqeq2d 
 |-  ( v = B -> ( ( A X. B ) = ( A X. v ) <-> ( A X. B ) = ( A X. B ) ) )
11 8 10 rspc2ev 
 |-  ( ( A e. R /\ B e. S /\ ( A X. B ) = ( A X. B ) ) -> E. u e. R E. v e. S ( A X. B ) = ( u X. v ) )
12 6 11 mp3an3 
 |-  ( ( A e. R /\ B e. S ) -> E. u e. R E. v e. S ( A X. B ) = ( u X. v ) )
13 xpexg 
 |-  ( ( A e. R /\ B e. S ) -> ( A X. B ) e. _V )
14 eqid 
 |-  ( u e. R , v e. S |-> ( u X. v ) ) = ( u e. R , v e. S |-> ( u X. v ) )
15 14 elrnmpog 
 |-  ( ( A X. B ) e. _V -> ( ( A X. B ) e. ran ( u e. R , v e. S |-> ( u X. v ) ) <-> E. u e. R E. v e. S ( A X. B ) = ( u X. v ) ) )
16 13 15 syl 
 |-  ( ( A e. R /\ B e. S ) -> ( ( A X. B ) e. ran ( u e. R , v e. S |-> ( u X. v ) ) <-> E. u e. R E. v e. S ( A X. B ) = ( u X. v ) ) )
17 12 16 mpbird 
 |-  ( ( A e. R /\ B e. S ) -> ( A X. B ) e. ran ( u e. R , v e. S |-> ( u X. v ) ) )
18 17 adantl 
 |-  ( ( ( R e. V /\ S e. W ) /\ ( A e. R /\ B e. S ) ) -> ( A X. B ) e. ran ( u e. R , v e. S |-> ( u X. v ) ) )
19 5 18 sseldd 
 |-  ( ( ( R e. V /\ S e. W ) /\ ( A e. R /\ B e. S ) ) -> ( A X. B ) e. ( topGen ` ran ( u e. R , v e. S |-> ( u X. v ) ) ) )
20 1 txval 
 |-  ( ( R e. V /\ S e. W ) -> ( R tX S ) = ( topGen ` ran ( u e. R , v e. S |-> ( u X. v ) ) ) )
21 20 adantr 
 |-  ( ( ( R e. V /\ S e. W ) /\ ( A e. R /\ B e. S ) ) -> ( R tX S ) = ( topGen ` ran ( u e. R , v e. S |-> ( u X. v ) ) ) )
22 19 21 eleqtrrd 
 |-  ( ( ( R e. V /\ S e. W ) /\ ( A e. R /\ B e. S ) ) -> ( A X. B ) e. ( R tX S ) )