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=HomaC
homahom.j J=HomC
Assertion homahom FXHY2ndFXJY

Proof

Step Hyp Ref Expression
1 homahom.h H=HomaC
2 homahom.j J=HomC
3 1 homarel RelXHY
4 1st2ndbr RelXHYFXHY1stFXHY2ndF
5 3 4 mpan FXHY1stFXHY2ndF
6 1 2 homahom2 1stFXHY2ndF2ndFXJY
7 5 6 syl FXHY2ndFXJY