Metamath Proof Explorer


Theorem fnhomeqhomf

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 )

Proof

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 )