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 = Hom 𝑓 C
homffval.b B = Base C
homffval.h H = Hom C
Assertion fnhomeqhomf H Fn B × B F = H

Proof

Step Hyp Ref Expression
1 homffval.f F = Hom 𝑓 C
2 homffval.b B = Base C
3 homffval.h H = Hom C
4 fnov H Fn B × B H = x B , y B x H y
5 1 2 3 homffval F = x B , y B x H y
6 eqeq2 H = x B , y B x H y F = H F = x B , y B x H y
7 5 6 mpbiri H = x B , y B x H y F = H
8 4 7 sylbi H Fn B × B F = H