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