Theorem hof1fval

Description: The object part of the Hom functor is the Homf operation, which is just a functionalized version of Hom . That is, it is a two argument function, which maps X , Y to the set of morphisms from X to Y . (Contributed by Mario Carneiro, 15-Jan-2017)

	Ref	Expression
Hypotheses	hofval.m	|- M = ( HomF ` C )
	hofval.c	|- ( ph -> C e. Cat )
Assertion	hof1fval	|- ( ph -> ( 1st ` M ) = ( Homf ` C ) )

Proof

Step	Hyp	Ref	Expression
1		hofval.m	|- M = ( HomF ` C )
2		hofval.c	|- ( ph -> C e. Cat )
3		eqid	|- ( Base ` C ) = ( Base ` C )
4		eqid	|- ( Hom ` C ) = ( Hom ` C )
5		eqid	|- ( comp ` C ) = ( comp ` C )
6	1 2 3 4 5	hofval	|- ( ph -> M = <. ( Homf ` C ) , ( x e. ( ( Base ` C ) X. ( Base ` C ) ) , y e. ( ( Base ` C ) X. ( Base ` C ) ) |-> ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) , g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) |-> ( h e. ( ( Hom ` C ) ` x ) |-> ( ( g ( x ( comp ` C ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. ( comp ` C ) ( 2nd ` y ) ) f ) ) ) ) >. )
7		fvex	|- ( Homf ` C ) e. _V
8		fvex	|- ( Base ` C ) e. _V
9	8 8	xpex	|- ( ( Base ` C ) X. ( Base ` C ) ) e. _V
10	9 9	mpoex	|- ( x e. ( ( Base ` C ) X. ( Base ` C ) ) , y e. ( ( Base ` C ) X. ( Base ` C ) ) |-> ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) , g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) |-> ( h e. ( ( Hom ` C ) ` x ) |-> ( ( g ( x ( comp ` C ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. ( comp ` C ) ( 2nd ` y ) ) f ) ) ) ) e. _V
11	7 10	op1std	|- ( M = <. ( Homf ` C ) , ( x e. ( ( Base ` C ) X. ( Base ` C ) ) , y e. ( ( Base ` C ) X. ( Base ` C ) ) |-> ( f e. ( ( 1st ` y ) ( Hom ` C ) ( 1st ` x ) ) , g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) |-> ( h e. ( ( Hom ` C ) ` x ) |-> ( ( g ( x ( comp ` C ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. ( comp ` C ) ( 2nd ` y ) ) f ) ) ) ) >. -> ( 1st ` M ) = ( Homf ` C ) )
12	6 11	syl	|- ( ph -> ( 1st ` M ) = ( Homf ` C ) )