Theorem homahom2

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	homahom2	|- ( Z ( X H Y ) F -> F e. ( X J Y ) )

Proof

Step	Hyp	Ref	Expression
1		homahom.h	|- H = ( HomA ` C )
2		homahom.j	|- J = ( Hom ` C )
3		df-br	|- ( Z ( X H Y ) F <-> <. Z , F >. e. ( X H Y ) )
4		eqid	|- ( Base ` C ) = ( Base ` C )
5	1	homarcl	|- ( <. Z , F >. e. ( X H Y ) -> C e. Cat )
6	1 4	homarcl2	|- ( <. Z , F >. e. ( X H Y ) -> ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) ) )
7	6	simpld	|- ( <. Z , F >. e. ( X H Y ) -> X e. ( Base ` C ) )
8	6	simprd	|- ( <. Z , F >. e. ( X H Y ) -> Y e. ( Base ` C ) )
9	1 4 5 2 7 8	elhoma	|- ( <. Z , F >. e. ( X H Y ) -> ( Z ( X H Y ) F <-> ( Z = <. X , Y >. /\ F e. ( X J Y ) ) ) )
10	3 9	sylbi	|- ( Z ( X H Y ) F -> ( Z ( X H Y ) F <-> ( Z = <. X , Y >. /\ F e. ( X J Y ) ) ) )
11	10	ibi	|- ( Z ( X H Y ) F -> ( Z = <. X , Y >. /\ F e. ( X J Y ) ) )
12	11	simprd	|- ( Z ( X H Y ) F -> F e. ( X J Y ) )