Theorem homacd

Description: The codomain of an arrow with known domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypothesis	homahom.h	|- H = ( HomA ` C )
Assertion	homacd	|- ( F e. ( X H Y ) -> ( codA ` F ) = Y )

Proof

Step	Hyp	Ref	Expression
1		homahom.h	|- H = ( HomA ` C )
2		df-coda	|- codA = ( 2nd o. 1st )
3	2	fveq1i	|- ( codA ` F ) = ( ( 2nd o. 1st ) ` F )
4		fo1st	|- 1st : _V -onto-> _V
5		fof	|- ( 1st : _V -onto-> _V -> 1st : _V --> _V )
6	4 5	ax-mp	|- 1st : _V --> _V
7		elex	|- ( F e. ( X H Y ) -> F e. _V )
8		fvco3	|- ( ( 1st : _V --> _V /\ F e. _V ) -> ( ( 2nd o. 1st ) ` F ) = ( 2nd ` ( 1st ` F ) ) )
9	6 7 8	sylancr	|- ( F e. ( X H Y ) -> ( ( 2nd o. 1st ) ` F ) = ( 2nd ` ( 1st ` F ) ) )
10	3 9	eqtrid	|- ( F e. ( X H Y ) -> ( codA ` F ) = ( 2nd ` ( 1st ` F ) ) )
11	1	homarel	|- Rel ( X H Y )
12		1st2ndbr	|- ( ( Rel ( X H Y ) /\ F e. ( X H Y ) ) -> ( 1st ` F ) ( X H Y ) ( 2nd ` F ) )
13	11 12	mpan	|- ( F e. ( X H Y ) -> ( 1st ` F ) ( X H Y ) ( 2nd ` F ) )
14	1	homa1	|- ( ( 1st ` F ) ( X H Y ) ( 2nd ` F ) -> ( 1st ` F ) = <. X , Y >. )
15	13 14	syl	|- ( F e. ( X H Y ) -> ( 1st ` F ) = <. X , Y >. )
16	15	fveq2d	|- ( F e. ( X H Y ) -> ( 2nd ` ( 1st ` F ) ) = ( 2nd ` <. X , Y >. ) )
17		eqid	|- ( Base ` C ) = ( Base ` C )
18	1 17	homarcl2	|- ( F e. ( X H Y ) -> ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) ) )
19		op2ndg	|- ( ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) ) -> ( 2nd ` <. X , Y >. ) = Y )
20	18 19	syl	|- ( F e. ( X H Y ) -> ( 2nd ` <. X , Y >. ) = Y )
21	10 16 20	3eqtrd	|- ( F e. ( X H Y ) -> ( codA ` F ) = Y )