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