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	|- .x. = ( compA ` C )
	homdmcoa.h	|- H = ( HomA ` C )
	homdmcoa.f	|- ( ph -> F e. ( X H Y ) )
	homdmcoa.g	|- ( ph -> G e. ( Y H Z ) )
Assertion	homdmcoa	|- ( ph -> G dom .x. F )

Proof

Step	Hyp	Ref	Expression
1		homdmcoa.o	|- .x. = ( compA ` C )
2		homdmcoa.h	|- H = ( HomA ` C )
3		homdmcoa.f	|- ( ph -> F e. ( X H Y ) )
4		homdmcoa.g	|- ( ph -> G e. ( Y H Z ) )
5		eqid	|- ( Arrow ` C ) = ( Arrow ` C )
6	5 2	homarw	|- ( X H Y ) C_ ( Arrow ` C )
7	6 3	sseldi	|- ( ph -> F e. ( Arrow ` C ) )
8	5 2	homarw	|- ( Y H Z ) C_ ( Arrow ` C )
9	8 4	sseldi	|- ( ph -> G e. ( Arrow ` C ) )
10	2	homacd	|- ( F e. ( X H Y ) -> ( codA ` F ) = Y )
11	3 10	syl	|- ( ph -> ( codA ` F ) = Y )
12	2	homadm	|- ( G e. ( Y H Z ) -> ( domA ` G ) = Y )
13	4 12	syl	|- ( ph -> ( domA ` G ) = Y )
14	11 13	eqtr4d	|- ( ph -> ( codA ` F ) = ( domA ` G ) )
15	1 5	eldmcoa	|- ( G dom .x. F <-> ( F e. ( Arrow ` C ) /\ G e. ( Arrow ` C ) /\ ( codA ` F ) = ( domA ` G ) ) )
16	7 9 14 15	syl3anbrc	|- ( ph -> G dom .x. F )