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