Step |
Hyp |
Ref |
Expression |
1 |
|
homarcl.h |
|- H = ( HomA ` C ) |
2 |
|
homafval.b |
|- B = ( Base ` C ) |
3 |
|
homafval.c |
|- ( ph -> C e. Cat ) |
4 |
|
homaval.j |
|- J = ( Hom ` C ) |
5 |
|
homaval.x |
|- ( ph -> X e. B ) |
6 |
|
homaval.y |
|- ( ph -> Y e. B ) |
7 |
|
df-ov |
|- ( X H Y ) = ( H ` <. X , Y >. ) |
8 |
1 2 3 4
|
homafval |
|- ( ph -> H = ( z e. ( B X. B ) |-> ( { z } X. ( J ` z ) ) ) ) |
9 |
|
simpr |
|- ( ( ph /\ z = <. X , Y >. ) -> z = <. X , Y >. ) |
10 |
9
|
sneqd |
|- ( ( ph /\ z = <. X , Y >. ) -> { z } = { <. X , Y >. } ) |
11 |
9
|
fveq2d |
|- ( ( ph /\ z = <. X , Y >. ) -> ( J ` z ) = ( J ` <. X , Y >. ) ) |
12 |
|
df-ov |
|- ( X J Y ) = ( J ` <. X , Y >. ) |
13 |
11 12
|
eqtr4di |
|- ( ( ph /\ z = <. X , Y >. ) -> ( J ` z ) = ( X J Y ) ) |
14 |
10 13
|
xpeq12d |
|- ( ( ph /\ z = <. X , Y >. ) -> ( { z } X. ( J ` z ) ) = ( { <. X , Y >. } X. ( X J Y ) ) ) |
15 |
5 6
|
opelxpd |
|- ( ph -> <. X , Y >. e. ( B X. B ) ) |
16 |
|
snex |
|- { <. X , Y >. } e. _V |
17 |
|
ovex |
|- ( X J Y ) e. _V |
18 |
16 17
|
xpex |
|- ( { <. X , Y >. } X. ( X J Y ) ) e. _V |
19 |
18
|
a1i |
|- ( ph -> ( { <. X , Y >. } X. ( X J Y ) ) e. _V ) |
20 |
8 14 15 19
|
fvmptd |
|- ( ph -> ( H ` <. X , Y >. ) = ( { <. X , Y >. } X. ( X J Y ) ) ) |
21 |
7 20
|
eqtrid |
|- ( ph -> ( X H Y ) = ( { <. X , Y >. } X. ( X J Y ) ) ) |