Step |
Hyp |
Ref |
Expression |
1 |
|
yonval.y |
|- Y = ( Yon ` C ) |
2 |
|
yonval.c |
|- ( ph -> C e. Cat ) |
3 |
|
yonval.o |
|- O = ( oppCat ` C ) |
4 |
|
yonval.m |
|- M = ( HomF ` O ) |
5 |
|
df-yon |
|- Yon = ( c e. Cat |-> ( <. c , ( oppCat ` c ) >. curryF ( HomF ` ( oppCat ` c ) ) ) ) |
6 |
|
simpr |
|- ( ( ph /\ c = C ) -> c = C ) |
7 |
6
|
fveq2d |
|- ( ( ph /\ c = C ) -> ( oppCat ` c ) = ( oppCat ` C ) ) |
8 |
7 3
|
eqtr4di |
|- ( ( ph /\ c = C ) -> ( oppCat ` c ) = O ) |
9 |
6 8
|
opeq12d |
|- ( ( ph /\ c = C ) -> <. c , ( oppCat ` c ) >. = <. C , O >. ) |
10 |
8
|
fveq2d |
|- ( ( ph /\ c = C ) -> ( HomF ` ( oppCat ` c ) ) = ( HomF ` O ) ) |
11 |
10 4
|
eqtr4di |
|- ( ( ph /\ c = C ) -> ( HomF ` ( oppCat ` c ) ) = M ) |
12 |
9 11
|
oveq12d |
|- ( ( ph /\ c = C ) -> ( <. c , ( oppCat ` c ) >. curryF ( HomF ` ( oppCat ` c ) ) ) = ( <. C , O >. curryF M ) ) |
13 |
|
ovexd |
|- ( ph -> ( <. C , O >. curryF M ) e. _V ) |
14 |
5 12 2 13
|
fvmptd2 |
|- ( ph -> ( Yon ` C ) = ( <. C , O >. curryF M ) ) |
15 |
1 14
|
eqtrid |
|- ( ph -> Y = ( <. C , O >. curryF M ) ) |