coahom

Description: The composition of two composable arrows is an arrow. (Contributed by Mario Carneiro, 11-Jan-2017)

Step	Hyp	Ref	Expression
1		homdmcoa.o	$⊢ \underset{˙}{\cdot} = {comp}_{a} (C)$
2		homdmcoa.h	$⊢ H = {Hom}_{a} (C)$
3		homdmcoa.f	$⊢ φ \to F \in (X H Y)$
4		homdmcoa.g	$⊢ φ \to G \in (Y H Z)$
5		eqid	$⊢ comp (C) = comp (C)$
6	1 2 3 4 5	coaval	$⊢ φ \to G \underset{˙}{\cdot} F = ⟨X, Z, 2^{nd} (G) (⟨X, Y⟩ comp (C) Z) 2^{nd} (F)⟩$
7		eqid	$⊢ {Base}_{C} = {Base}_{C}$
8	2	homarcl	$⊢ F \in (X H Y) \to C \in Cat$
9	3 8	syl	$⊢ φ \to C \in Cat$
10		eqid	$⊢ Hom (C) = Hom (C)$
11	2 7	homarcl2	$⊢ F \in (X H Y) \to (X \in {Base}_{C} \land Y \in {Base}_{C})$
12	3 11	syl	$⊢ φ \to (X \in {Base}_{C} \land Y \in {Base}_{C})$
13	12	simpld	$⊢ φ \to X \in {Base}_{C}$
14	2 7	homarcl2	$⊢ G \in (Y H Z) \to (Y \in {Base}_{C} \land Z \in {Base}_{C})$
15	4 14	syl	$⊢ φ \to (Y \in {Base}_{C} \land Z \in {Base}_{C})$
16	15	simprd	$⊢ φ \to Z \in {Base}_{C}$
17	12	simprd	$⊢ φ \to Y \in {Base}_{C}$
18	2 10	homahom	$⊢ F \in (X H Y) \to 2^{nd} (F) \in (X Hom (C) Y)$
19	3 18	syl	$⊢ φ \to 2^{nd} (F) \in (X Hom (C) Y)$
20	2 10	homahom	$⊢ G \in (Y H Z) \to 2^{nd} (G) \in (Y Hom (C) Z)$
21	4 20	syl	$⊢ φ \to 2^{nd} (G) \in (Y Hom (C) Z)$
22	7 10 5 9 13 17 16 19 21	catcocl	$⊢ φ \to 2^{nd} (G) (⟨X, Y⟩ comp (C) Z) 2^{nd} (F) \in (X Hom (C) Z)$
23	2 7 9 10 13 16 22	elhomai2	$⊢ φ \to ⟨X, Z, 2^{nd} (G) (⟨X, Y⟩ comp (C) Z) 2^{nd} (F)⟩ \in (X H Z)$
24	6 23	eqeltrd	$⊢ φ \to G \underset{˙}{\cdot} F \in (X H Z)$

Metamath Proof Explorer