Description: If the Hom-set operation is a function it is equal to the corresponding functionalized Hom-set operation. (Contributed by AV, 1-Mar-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | homffval.f | |- F = ( Homf ` C ) |
|
homffval.b | |- B = ( Base ` C ) |
||
homffval.h | |- H = ( Hom ` C ) |
||
Assertion | fnhomeqhomf | |- ( H Fn ( B X. B ) -> F = H ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | homffval.f | |- F = ( Homf ` C ) |
|
2 | homffval.b | |- B = ( Base ` C ) |
|
3 | homffval.h | |- H = ( Hom ` C ) |
|
4 | fnov | |- ( H Fn ( B X. B ) <-> H = ( x e. B , y e. B |-> ( x H y ) ) ) |
|
5 | 1 2 3 | homffval | |- F = ( x e. B , y e. B |-> ( x H y ) ) |
6 | eqeq2 | |- ( H = ( x e. B , y e. B |-> ( x H y ) ) -> ( F = H <-> F = ( x e. B , y e. B |-> ( x H y ) ) ) ) |
|
7 | 5 6 | mpbiri | |- ( H = ( x e. B , y e. B |-> ( x H y ) ) -> F = H ) |
8 | 4 7 | sylbi | |- ( H Fn ( B X. B ) -> F = H ) |