Step |
Hyp |
Ref |
Expression |
1 |
|
setcbas.c |
|- C = ( SetCat ` U ) |
2 |
|
setcbas.u |
|- ( ph -> U e. V ) |
3 |
|
setchomfval.h |
|- H = ( Hom ` C ) |
4 |
|
eqidd |
|- ( ph -> ( x e. U , y e. U |-> ( y ^m x ) ) = ( x e. U , y e. U |-> ( y ^m x ) ) ) |
5 |
|
eqidd |
|- ( ph -> ( v e. ( U X. U ) , z e. U |-> ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) ) ) = ( v e. ( U X. U ) , z e. U |-> ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) ) ) ) |
6 |
1 2 4 5
|
setcval |
|- ( ph -> C = { <. ( Base ` ndx ) , U >. , <. ( Hom ` ndx ) , ( x e. U , y e. U |-> ( y ^m x ) ) >. , <. ( comp ` ndx ) , ( v e. ( U X. U ) , z e. U |-> ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) ) ) >. } ) |
7 |
|
catstr |
|- { <. ( Base ` ndx ) , U >. , <. ( Hom ` ndx ) , ( x e. U , y e. U |-> ( y ^m x ) ) >. , <. ( comp ` ndx ) , ( v e. ( U X. U ) , z e. U |-> ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) ) ) >. } Struct <. 1 , ; 1 5 >. |
8 |
|
homid |
|- Hom = Slot ( Hom ` ndx ) |
9 |
|
snsstp2 |
|- { <. ( Hom ` ndx ) , ( x e. U , y e. U |-> ( y ^m x ) ) >. } C_ { <. ( Base ` ndx ) , U >. , <. ( Hom ` ndx ) , ( x e. U , y e. U |-> ( y ^m x ) ) >. , <. ( comp ` ndx ) , ( v e. ( U X. U ) , z e. U |-> ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) ) ) >. } |
10 |
|
mpoexga |
|- ( ( U e. V /\ U e. V ) -> ( x e. U , y e. U |-> ( y ^m x ) ) e. _V ) |
11 |
2 2 10
|
syl2anc |
|- ( ph -> ( x e. U , y e. U |-> ( y ^m x ) ) e. _V ) |
12 |
6 7 8 9 11 3
|
strfv3 |
|- ( ph -> H = ( x e. U , y e. U |-> ( y ^m x ) ) ) |