Metamath Proof Explorer


Theorem homahom

Description: The second component of an arrow is the corresponding morphism (without the domain/codomain tag). (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypotheses homahom.h H = Hom a C
homahom.j J = Hom C
Assertion homahom F X H Y 2 nd F X J Y

Proof

Step Hyp Ref Expression
1 homahom.h H = Hom a C
2 homahom.j J = Hom C
3 1 homarel Rel X H Y
4 1st2ndbr Rel X H Y F X H Y 1 st F X H Y 2 nd F
5 3 4 mpan F X H Y 1 st F X H Y 2 nd F
6 1 2 homahom2 1 st F X H Y 2 nd F 2 nd F X J Y
7 5 6 syl F X H Y 2 nd F X J Y