Definition df-homf

Description: Define the functionalized Hom-set operator, which is exactly like Hom but is guaranteed to be a function on the base. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Assertion	df-homf	|- Homf = ( c e. _V |-> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> ( x ( Hom ` c ) y ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chomf	|- Homf
1		vc	|- c
2		cvv	|- _V
3		vx	|- x
4		cbs	|- Base
5	1	cv	|- c
6	5 4	cfv	|- ( Base ` c )
7		vy	|- y
8	3	cv	|- x
9		chom	|- Hom
10	5 9	cfv	|- ( Hom ` c )
11	7	cv	|- y
12	8 11 10	co	|- ( x ( Hom ` c ) y )
13	3 7 6 6 12	cmpo	|- ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> ( x ( Hom ` c ) y ) )
14	1 2 13	cmpt	|- ( c e. _V |-> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> ( x ( Hom ` c ) y ) ) )
15	0 14	wceq	|- Homf = ( c e. _V |-> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> ( x ( Hom ` c ) y ) ) )