Theorem homfval

Description: Value of the functionalized Hom-set operation. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Hypotheses	homffval.f	|- F = ( Homf ` C )
	homffval.b	|- B = ( Base ` C )
	homffval.h	|- H = ( Hom ` C )
	homfval.x	|- ( ph -> X e. B )
	homfval.y	|- ( ph -> Y e. B )
Assertion	homfval	|- ( ph -> ( X F Y ) = ( X H Y ) )

Proof

Step	Hyp	Ref	Expression
1		homffval.f	|- F = ( Homf ` C )
2		homffval.b	|- B = ( Base ` C )
3		homffval.h	|- H = ( Hom ` C )
4		homfval.x	|- ( ph -> X e. B )
5		homfval.y	|- ( ph -> Y e. B )
6	1 2 3	homffval	|- F = ( x e. B , y e. B |-> ( x H y ) )
7	6	a1i	|- ( ph -> F = ( x e. B , y e. B |-> ( x H y ) ) )
8		oveq12	|- ( ( x = X /\ y = Y ) -> ( x H y ) = ( X H Y ) )
9	8	adantl	|- ( ( ph /\ ( x = X /\ y = Y ) ) -> ( x H y ) = ( X H Y ) )
10		ovexd	|- ( ph -> ( X H Y ) e. _V )
11	7 9 4 5 10	ovmpod	|- ( ph -> ( X F Y ) = ( X H Y ) )