Theorem hof1

Description: The object part of the Hom functor 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 )
	hof1.b	|- B = ( Base ` C )
	hof1.h	|- H = ( Hom ` C )
	hof1.x	|- ( ph -> X e. B )
	hof1.y	|- ( ph -> Y e. B )
Assertion	hof1	|- ( ph -> ( X ( 1st ` M ) Y ) = ( X H Y ) )

Proof

Step	Hyp	Ref	Expression
1		hofval.m	|- M = ( HomF ` C )
2		hofval.c	|- ( ph -> C e. Cat )
3		hof1.b	|- B = ( Base ` C )
4		hof1.h	|- H = ( Hom ` C )
5		hof1.x	|- ( ph -> X e. B )
6		hof1.y	|- ( ph -> Y e. B )
7	1 2	hof1fval	|- ( ph -> ( 1st ` M ) = ( Homf ` C ) )
8	7	oveqd	|- ( ph -> ( X ( 1st ` M ) Y ) = ( X ( Homf ` C ) Y ) )
9		eqid	|- ( Homf ` C ) = ( Homf ` C )
10	9 3 4 5 6	homfval	|- ( ph -> ( X ( Homf ` C ) Y ) = ( X H Y ) )
11	8 10	eqtrd	|- ( ph -> ( X ( 1st ` M ) Y ) = ( X H Y ) )