Theorem elhomai2

Description: Produce an arrow from a morphism. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	homarcl.h	|- H = ( HomA ` C )
	homafval.b	|- B = ( Base ` C )
	homafval.c	|- ( ph -> C e. Cat )
	homaval.j	|- J = ( Hom ` C )
	homaval.x	|- ( ph -> X e. B )
	homaval.y	|- ( ph -> Y e. B )
	elhomai.f	|- ( ph -> F e. ( X J Y ) )
Assertion	elhomai2	|- ( ph -> <. X , Y , F >. e. ( X H Y ) )

Proof

Step	Hyp	Ref	Expression
1		homarcl.h	|- H = ( HomA ` C )
2		homafval.b	|- B = ( Base ` C )
3		homafval.c	|- ( ph -> C e. Cat )
4		homaval.j	|- J = ( Hom ` C )
5		homaval.x	|- ( ph -> X e. B )
6		homaval.y	|- ( ph -> Y e. B )
7		elhomai.f	|- ( ph -> F e. ( X J Y ) )
8		df-ot	|- <. X , Y , F >. = <. <. X , Y >. , F >.
9	1 2 3 4 5 6 7	elhomai	|- ( ph -> <. X , Y >. ( X H Y ) F )
10		df-br	|- ( <. X , Y >. ( X H Y ) F <-> <. <. X , Y >. , F >. e. ( X H Y ) )
11	9 10	sylib	|- ( ph -> <. <. X , Y >. , F >. e. ( X H Y ) )
12	8 11	eqeltrid	|- ( ph -> <. X , Y , F >. e. ( X H Y ) )