Metamath Proof Explorer

Theorem txval

Description: Value of the binary topological product operation. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 30-Aug-2015)

Ref Expression
Hypothesis txval.1 
|- B = ran ( x e. R , y e. S |-> ( x X. y ) )
Assertion txval 
|- ( ( R e. V /\ S e. W ) -> ( R tX S ) = ( topGen ` B ) )

Proof

Step Hyp Ref Expression
1 txval.1 
 |-  B = ran ( x e. R , y e. S |-> ( x X. y ) )
2 elex 
 |-  ( R e. V -> R e. _V )
3 elex 
 |-  ( S e. W -> S e. _V )
4 mpoeq12 
 |-  ( ( r = R /\ s = S ) -> ( x e. r , y e. s |-> ( x X. y ) ) = ( x e. R , y e. S |-> ( x X. y ) ) )
5 4 rneqd 
 |-  ( ( r = R /\ s = S ) -> ran ( x e. r , y e. s |-> ( x X. y ) ) = ran ( x e. R , y e. S |-> ( x X. y ) ) )
6 5 1 eqtr4di 
 |-  ( ( r = R /\ s = S ) -> ran ( x e. r , y e. s |-> ( x X. y ) ) = B )
7 6 fveq2d 
 |-  ( ( r = R /\ s = S ) -> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) = ( topGen ` B ) )
8 df-tx 
 |-  tX = ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )
9 fvex 
 |-  ( topGen ` B ) e. _V
10 7 8 9 ovmpoa 
 |-  ( ( R e. _V /\ S e. _V ) -> ( R tX S ) = ( topGen ` B ) )
11 2 3 10 syl2an 
 |-  ( ( R e. V /\ S e. W ) -> ( R tX S ) = ( topGen ` B ) )