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 = ( HomA ` C )
	homahom.j	|- J = ( Hom ` C )
Assertion	homahom	|- ( F e. ( X H Y ) -> ( 2nd ` F ) e. ( X J Y ) )

Proof

Step	Hyp	Ref	Expression
1		homahom.h	|- H = ( HomA ` C )
2		homahom.j	|- J = ( Hom ` C )
3	1	homarel	|- Rel ( X H Y )
4		1st2ndbr	|- ( ( Rel ( X H Y ) /\ F e. ( X H Y ) ) -> ( 1st ` F ) ( X H Y ) ( 2nd ` F ) )
5	3 4	mpan	|- ( F e. ( X H Y ) -> ( 1st ` F ) ( X H Y ) ( 2nd ` F ) )
6	1 2	homahom2	|- ( ( 1st ` F ) ( X H Y ) ( 2nd ` F ) -> ( 2nd ` F ) e. ( X J Y ) )
7	5 6	syl	|- ( F e. ( X H Y ) -> ( 2nd ` F ) e. ( X J Y ) )