Metamath Proof Explorer

Theorem txbasval

Description: It is sufficient to consider products of the bases for the topologies in the topological product. (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Assertion txbasval 
|- ( ( R e. V /\ S e. W ) -> ( ( topGen ` R ) tX ( topGen ` S ) ) = ( 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 txval 
 |-  ( ( R e. V /\ S e. W ) -> ( R tX S ) = ( topGen ` ran ( u e. R , v e. S |-> ( u X. v ) ) ) )
3 bastg 
 |-  ( R e. V -> R C_ ( topGen ` R ) )
4 bastg 
 |-  ( S e. W -> S C_ ( topGen ` S ) )
5 resmpo 
 |-  ( ( R C_ ( topGen ` R ) /\ S C_ ( topGen ` S ) ) -> ( ( u e. ( topGen ` R ) , v e. ( topGen ` S ) |-> ( u X. v ) ) |` ( R X. S ) ) = ( u e. R , v e. S |-> ( u X. v ) ) )
6 3 4 5 syl2an 
 |-  ( ( R e. V /\ S e. W ) -> ( ( u e. ( topGen ` R ) , v e. ( topGen ` S ) |-> ( u X. v ) ) |` ( R X. S ) ) = ( u e. R , v e. S |-> ( u X. v ) ) )
7 resss 
 |-  ( ( u e. ( topGen ` R ) , v e. ( topGen ` S ) |-> ( u X. v ) ) |` ( R X. S ) ) C_ ( u e. ( topGen ` R ) , v e. ( topGen ` S ) |-> ( u X. v ) )
8 6 7 eqsstrrdi 
 |-  ( ( R e. V /\ S e. W ) -> ( u e. R , v e. S |-> ( u X. v ) ) C_ ( u e. ( topGen ` R ) , v e. ( topGen ` S ) |-> ( u X. v ) ) )
9 rnss 
 |-  ( ( u e. R , v e. S |-> ( u X. v ) ) C_ ( u e. ( topGen ` R ) , v e. ( topGen ` S ) |-> ( u X. v ) ) -> ran ( u e. R , v e. S |-> ( u X. v ) ) C_ ran ( u e. ( topGen ` R ) , v e. ( topGen ` S ) |-> ( u X. v ) ) )
10 8 9 syl 
 |-  ( ( R e. V /\ S e. W ) -> ran ( u e. R , v e. S |-> ( u X. v ) ) C_ ran ( u e. ( topGen ` R ) , v e. ( topGen ` S ) |-> ( u X. v ) ) )
11 eltg3 
 |-  ( R e. V -> ( u e. ( topGen ` R ) <-> E. m ( m C_ R /\ u = U. m ) ) )
12 eltg3 
 |-  ( S e. W -> ( v e. ( topGen ` S ) <-> E. n ( n C_ S /\ v = U. n ) ) )
13 11 12 bi2anan9 
 |-  ( ( R e. V /\ S e. W ) -> ( ( u e. ( topGen ` R ) /\ v e. ( topGen ` S ) ) <-> ( E. m ( m C_ R /\ u = U. m ) /\ E. n ( n C_ S /\ v = U. n ) ) ) )
14 exdistrv 
 |-  ( E. m E. n ( ( m C_ R /\ u = U. m ) /\ ( n C_ S /\ v = U. n ) ) <-> ( E. m ( m C_ R /\ u = U. m ) /\ E. n ( n C_ S /\ v = U. n ) ) )
15 an4 
 |-  ( ( ( m C_ R /\ u = U. m ) /\ ( n C_ S /\ v = U. n ) ) <-> ( ( m C_ R /\ n C_ S ) /\ ( u = U. m /\ v = U. n ) ) )
16 uniiun 
 |-  U. m = U_ x e. m x
17 uniiun 
 |-  U. n = U_ y e. n y
18 16 17 xpeq12i 
 |-  ( U. m X. U. n ) = ( U_ x e. m x X. U_ y e. n y )
19 xpiundir 
 |-  ( U_ x e. m x X. U_ y e. n y ) = U_ x e. m ( x X. U_ y e. n y )
20 xpiundi 
 |-  ( x X. U_ y e. n y ) = U_ y e. n ( x X. y )
21 20 a1i 
 |-  ( x e. m -> ( x X. U_ y e. n y ) = U_ y e. n ( x X. y ) )
22 21 iuneq2i 
 |-  U_ x e. m ( x X. U_ y e. n y ) = U_ x e. m U_ y e. n ( x X. y )
23 18 19 22 3eqtri 
 |-  ( U. m X. U. n ) = U_ x e. m U_ y e. n ( x X. y )
24 ovex 
 |-  ( R tX S ) e. _V
25 ssel2 
 |-  ( ( m C_ R /\ x e. m ) -> x e. R )
26 ssel2 
 |-  ( ( n C_ S /\ y e. n ) -> y e. S )
27 25 26 anim12i 
 |-  ( ( ( m C_ R /\ x e. m ) /\ ( n C_ S /\ y e. n ) ) -> ( x e. R /\ y e. S ) )
28 27 an4s 
 |-  ( ( ( m C_ R /\ n C_ S ) /\ ( x e. m /\ y e. n ) ) -> ( x e. R /\ y e. S ) )
29 txopn 
 |-  ( ( ( R e. V /\ S e. W ) /\ ( x e. R /\ y e. S ) ) -> ( x X. y ) e. ( R tX S ) )
30 28 29 sylan2 
 |-  ( ( ( R e. V /\ S e. W ) /\ ( ( m C_ R /\ n C_ S ) /\ ( x e. m /\ y e. n ) ) ) -> ( x X. y ) e. ( R tX S ) )
31 30 anassrs 
 |-  ( ( ( ( R e. V /\ S e. W ) /\ ( m C_ R /\ n C_ S ) ) /\ ( x e. m /\ y e. n ) ) -> ( x X. y ) e. ( R tX S ) )
32 31 anassrs 
 |-  ( ( ( ( ( R e. V /\ S e. W ) /\ ( m C_ R /\ n C_ S ) ) /\ x e. m ) /\ y e. n ) -> ( x X. y ) e. ( R tX S ) )
33 32 ralrimiva 
 |-  ( ( ( ( R e. V /\ S e. W ) /\ ( m C_ R /\ n C_ S ) ) /\ x e. m ) -> A. y e. n ( x X. y ) e. ( R tX S ) )
34 tgiun 
 |-  ( ( ( R tX S ) e. _V /\ A. y e. n ( x X. y ) e. ( R tX S ) ) -> U_ y e. n ( x X. y ) e. ( topGen ` ( R tX S ) ) )
35 24 33 34 sylancr 
 |-  ( ( ( ( R e. V /\ S e. W ) /\ ( m C_ R /\ n C_ S ) ) /\ x e. m ) -> U_ y e. n ( x X. y ) e. ( topGen ` ( R tX S ) ) )
36 1 txbasex 
 |-  ( ( R e. V /\ S e. W ) -> ran ( u e. R , v e. S |-> ( u X. v ) ) e. _V )
37 tgidm 
 |-  ( ran ( u e. R , v e. S |-> ( u X. v ) ) e. _V -> ( topGen ` ( topGen ` ran ( u e. R , v e. S |-> ( u X. v ) ) ) ) = ( topGen ` ran ( u e. R , v e. S |-> ( u X. v ) ) ) )
38 36 37 syl 
 |-  ( ( R e. V /\ S e. W ) -> ( topGen ` ( topGen ` ran ( u e. R , v e. S |-> ( u X. v ) ) ) ) = ( topGen ` ran ( u e. R , v e. S |-> ( u X. v ) ) ) )
39 2 fveq2d 
 |-  ( ( R e. V /\ S e. W ) -> ( topGen ` ( R tX S ) ) = ( topGen ` ( topGen ` ran ( u e. R , v e. S |-> ( u X. v ) ) ) ) )
40 38 39 2 3eqtr4d 
 |-  ( ( R e. V /\ S e. W ) -> ( topGen ` ( R tX S ) ) = ( R tX S ) )
41 40 adantr 
 |-  ( ( ( R e. V /\ S e. W ) /\ ( m C_ R /\ n C_ S ) ) -> ( topGen ` ( R tX S ) ) = ( R tX S ) )
42 41 adantr 
 |-  ( ( ( ( R e. V /\ S e. W ) /\ ( m C_ R /\ n C_ S ) ) /\ x e. m ) -> ( topGen ` ( R tX S ) ) = ( R tX S ) )
43 35 42 eleqtrd 
 |-  ( ( ( ( R e. V /\ S e. W ) /\ ( m C_ R /\ n C_ S ) ) /\ x e. m ) -> U_ y e. n ( x X. y ) e. ( R tX S ) )
44 43 ralrimiva 
 |-  ( ( ( R e. V /\ S e. W ) /\ ( m C_ R /\ n C_ S ) ) -> A. x e. m U_ y e. n ( x X. y ) e. ( R tX S ) )
45 tgiun 
 |-  ( ( ( R tX S ) e. _V /\ A. x e. m U_ y e. n ( x X. y ) e. ( R tX S ) ) -> U_ x e. m U_ y e. n ( x X. y ) e. ( topGen ` ( R tX S ) ) )
46 24 44 45 sylancr 
 |-  ( ( ( R e. V /\ S e. W ) /\ ( m C_ R /\ n C_ S ) ) -> U_ x e. m U_ y e. n ( x X. y ) e. ( topGen ` ( R tX S ) ) )
47 46 41 eleqtrd 
 |-  ( ( ( R e. V /\ S e. W ) /\ ( m C_ R /\ n C_ S ) ) -> U_ x e. m U_ y e. n ( x X. y ) e. ( R tX S ) )
48 23 47 eqeltrid 
 |-  ( ( ( R e. V /\ S e. W ) /\ ( m C_ R /\ n C_ S ) ) -> ( U. m X. U. n ) e. ( R tX S ) )
49 xpeq12 
 |-  ( ( u = U. m /\ v = U. n ) -> ( u X. v ) = ( U. m X. U. n ) )
50 49 eleq1d 
 |-  ( ( u = U. m /\ v = U. n ) -> ( ( u X. v ) e. ( R tX S ) <-> ( U. m X. U. n ) e. ( R tX S ) ) )
51 48 50 syl5ibrcom 
 |-  ( ( ( R e. V /\ S e. W ) /\ ( m C_ R /\ n C_ S ) ) -> ( ( u = U. m /\ v = U. n ) -> ( u X. v ) e. ( R tX S ) ) )
52 51 expimpd 
 |-  ( ( R e. V /\ S e. W ) -> ( ( ( m C_ R /\ n C_ S ) /\ ( u = U. m /\ v = U. n ) ) -> ( u X. v ) e. ( R tX S ) ) )
53 15 52 syl5bi 
 |-  ( ( R e. V /\ S e. W ) -> ( ( ( m C_ R /\ u = U. m ) /\ ( n C_ S /\ v = U. n ) ) -> ( u X. v ) e. ( R tX S ) ) )
54 53 exlimdvv 
 |-  ( ( R e. V /\ S e. W ) -> ( E. m E. n ( ( m C_ R /\ u = U. m ) /\ ( n C_ S /\ v = U. n ) ) -> ( u X. v ) e. ( R tX S ) ) )
55 14 54 syl5bir 
 |-  ( ( R e. V /\ S e. W ) -> ( ( E. m ( m C_ R /\ u = U. m ) /\ E. n ( n C_ S /\ v = U. n ) ) -> ( u X. v ) e. ( R tX S ) ) )
56 13 55 sylbid 
 |-  ( ( R e. V /\ S e. W ) -> ( ( u e. ( topGen ` R ) /\ v e. ( topGen ` S ) ) -> ( u X. v ) e. ( R tX S ) ) )
57 56 ralrimivv 
 |-  ( ( R e. V /\ S e. W ) -> A. u e. ( topGen ` R ) A. v e. ( topGen ` S ) ( u X. v ) e. ( R tX S ) )
58 eqid 
 |-  ( u e. ( topGen ` R ) , v e. ( topGen ` S ) |-> ( u X. v ) ) = ( u e. ( topGen ` R ) , v e. ( topGen ` S ) |-> ( u X. v ) )
59 58 fmpo 
 |-  ( A. u e. ( topGen ` R ) A. v e. ( topGen ` S ) ( u X. v ) e. ( R tX S ) <-> ( u e. ( topGen ` R ) , v e. ( topGen ` S ) |-> ( u X. v ) ) : ( ( topGen ` R ) X. ( topGen ` S ) ) --> ( R tX S ) )
60 57 59 sylib 
 |-  ( ( R e. V /\ S e. W ) -> ( u e. ( topGen ` R ) , v e. ( topGen ` S ) |-> ( u X. v ) ) : ( ( topGen ` R ) X. ( topGen ` S ) ) --> ( R tX S ) )
61 60 frnd 
 |-  ( ( R e. V /\ S e. W ) -> ran ( u e. ( topGen ` R ) , v e. ( topGen ` S ) |-> ( u X. v ) ) C_ ( R tX S ) )
62 61 2 sseqtrd 
 |-  ( ( R e. V /\ S e. W ) -> ran ( u e. ( topGen ` R ) , v e. ( topGen ` S ) |-> ( u X. v ) ) C_ ( topGen ` ran ( u e. R , v e. S |-> ( u X. v ) ) ) )
63 2basgen 
 |-  ( ( ran ( u e. R , v e. S |-> ( u X. v ) ) C_ ran ( u e. ( topGen ` R ) , v e. ( topGen ` S ) |-> ( u X. v ) ) /\ ran ( u e. ( topGen ` R ) , v e. ( topGen ` S ) |-> ( u X. v ) ) C_ ( topGen ` ran ( u e. R , v e. S |-> ( u X. v ) ) ) ) -> ( topGen ` ran ( u e. R , v e. S |-> ( u X. v ) ) ) = ( topGen ` ran ( u e. ( topGen ` R ) , v e. ( topGen ` S ) |-> ( u X. v ) ) ) )
64 10 62 63 syl2anc 
 |-  ( ( R e. V /\ S e. W ) -> ( topGen ` ran ( u e. R , v e. S |-> ( u X. v ) ) ) = ( topGen ` ran ( u e. ( topGen ` R ) , v e. ( topGen ` S ) |-> ( u X. v ) ) ) )
65 fvex 
 |-  ( topGen ` R ) e. _V
66 fvex 
 |-  ( topGen ` S ) e. _V
67 eqid 
 |-  ran ( u e. ( topGen ` R ) , v e. ( topGen ` S ) |-> ( u X. v ) ) = ran ( u e. ( topGen ` R ) , v e. ( topGen ` S ) |-> ( u X. v ) )
68 67 txval 
 |-  ( ( ( topGen ` R ) e. _V /\ ( topGen ` S ) e. _V ) -> ( ( topGen ` R ) tX ( topGen ` S ) ) = ( topGen ` ran ( u e. ( topGen ` R ) , v e. ( topGen ` S ) |-> ( u X. v ) ) ) )
69 65 66 68 mp2an 
 |-  ( ( topGen ` R ) tX ( topGen ` S ) ) = ( topGen ` ran ( u e. ( topGen ` R ) , v e. ( topGen ` S ) |-> ( u X. v ) ) )
70 64 69 eqtr4di 
 |-  ( ( R e. V /\ S e. W ) -> ( topGen ` ran ( u e. R , v e. S |-> ( u X. v ) ) ) = ( ( topGen ` R ) tX ( topGen ` S ) ) )
71 2 70 eqtr2d 
 |-  ( ( R e. V /\ S e. W ) -> ( ( topGen ` R ) tX ( topGen ` S ) ) = ( R tX S ) )