Metamath Proof Explorer


Theorem homdmcoa

Description: If F : X --> Y and G : Y --> Z , then G and F are composable. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypotheses homdmcoa.o · ˙ = comp a C
homdmcoa.h H = Hom a C
homdmcoa.f φ F X H Y
homdmcoa.g φ G Y H Z
Assertion homdmcoa φ G dom · ˙ F

Proof

Step Hyp Ref Expression
1 homdmcoa.o · ˙ = comp a C
2 homdmcoa.h H = Hom a C
3 homdmcoa.f φ F X H Y
4 homdmcoa.g φ G Y H Z
5 eqid Arrow C = Arrow C
6 5 2 homarw X H Y Arrow C
7 6 3 sselid φ F Arrow C
8 5 2 homarw Y H Z Arrow C
9 8 4 sselid φ G Arrow C
10 2 homacd F X H Y cod a F = Y
11 3 10 syl φ cod a F = Y
12 2 homadm G Y H Z dom a G = Y
13 4 12 syl φ dom a G = Y
14 11 13 eqtr4d φ cod a F = dom a G
15 1 5 eldmcoa G dom · ˙ F F Arrow C G Arrow C cod a F = dom a G
16 7 9 14 15 syl3anbrc φ G dom · ˙ F