Theorem homffn

Description: The functionalized Hom-set operation is a function. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Hypotheses	homffn.f	|- F = ( Homf ` C )
	homffn.b	|- B = ( Base ` C )
Assertion	homffn	|- F Fn ( B X. B )

Proof

Step	Hyp	Ref	Expression
1		homffn.f	|- F = ( Homf ` C )
2		homffn.b	|- B = ( Base ` C )
3		eqid	|- ( Hom ` C ) = ( Hom ` C )
4	1 2 3	homffval	|- F = ( x e. B , y e. B |-> ( x ( Hom ` C ) y ) )
5		ovex	|- ( x ( Hom ` C ) y ) e. _V
6	4 5	fnmpoi	|- F Fn ( B X. B )