Step |
Hyp |
Ref |
Expression |
1 |
|
ucnprima.1 |
|- ( ph -> U e. ( UnifOn ` X ) ) |
2 |
|
ucnprima.2 |
|- ( ph -> V e. ( UnifOn ` Y ) ) |
3 |
|
ucnprima.3 |
|- ( ph -> F e. ( U uCn V ) ) |
4 |
|
ucnprima.4 |
|- ( ph -> W e. V ) |
5 |
|
ucnprima.5 |
|- G = ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) |
6 |
|
vex |
|- x e. _V |
7 |
|
vex |
|- y e. _V |
8 |
6 7
|
op1std |
|- ( p = <. x , y >. -> ( 1st ` p ) = x ) |
9 |
8
|
fveq2d |
|- ( p = <. x , y >. -> ( F ` ( 1st ` p ) ) = ( F ` x ) ) |
10 |
6 7
|
op2ndd |
|- ( p = <. x , y >. -> ( 2nd ` p ) = y ) |
11 |
10
|
fveq2d |
|- ( p = <. x , y >. -> ( F ` ( 2nd ` p ) ) = ( F ` y ) ) |
12 |
9 11
|
opeq12d |
|- ( p = <. x , y >. -> <. ( F ` ( 1st ` p ) ) , ( F ` ( 2nd ` p ) ) >. = <. ( F ` x ) , ( F ` y ) >. ) |
13 |
12
|
mpompt |
|- ( p e. ( X X. X ) |-> <. ( F ` ( 1st ` p ) ) , ( F ` ( 2nd ` p ) ) >. ) = ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) |
14 |
5 13
|
eqtr4i |
|- G = ( p e. ( X X. X ) |-> <. ( F ` ( 1st ` p ) ) , ( F ` ( 2nd ` p ) ) >. ) |