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