Theorem homffval

Description: Value of the functionalized Hom-set operation. (Contributed by Mario Carneiro, 4-Jan-2017) (Proof shortened by AV, 1-Mar-2024)

	Ref	Expression
Hypotheses	homffval.f	|- F = ( Homf ` C )
	homffval.b	|- B = ( Base ` C )
	homffval.h	|- H = ( Hom ` C )
Assertion	homffval	|- F = ( x e. B , y e. B |-> ( 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		fveq2	|- ( c = C -> ( Base ` c ) = ( Base ` C ) )
5	4 2	eqtr4di	|- ( c = C -> ( Base ` c ) = B )
6		fveq2	|- ( c = C -> ( Hom ` c ) = ( Hom ` C ) )
7	6 3	eqtr4di	|- ( c = C -> ( Hom ` c ) = H )
8	7	oveqd	|- ( c = C -> ( x ( Hom ` c ) y ) = ( x H y ) )
9	5 5 8	mpoeq123dv	|- ( c = C -> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> ( x ( Hom ` c ) y ) ) = ( x e. B , y e. B |-> ( x H y ) ) )
10		df-homf	|- Homf = ( c e. _V |-> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> ( x ( Hom ` c ) y ) ) )
11	2	fvexi	|- B e. _V
12	11 11	mpoex	|- ( x e. B , y e. B |-> ( x H y ) ) e. _V
13	9 10 12	fvmpt	|- ( C e. _V -> ( Homf ` C ) = ( x e. B , y e. B |-> ( x H y ) ) )
14		fvprc	|- ( -. C e. _V -> ( Homf ` C ) = (/) )
15		fvprc	|- ( -. C e. _V -> ( Base ` C ) = (/) )
16	2 15	syl5eq	|- ( -. C e. _V -> B = (/) )
17	16	olcd	|- ( -. C e. _V -> ( B = (/) \/ B = (/) ) )
18		0mpo0	|- ( ( B = (/) \/ B = (/) ) -> ( x e. B , y e. B |-> ( x H y ) ) = (/) )
19	17 18	syl	|- ( -. C e. _V -> ( x e. B , y e. B |-> ( x H y ) ) = (/) )
20	14 19	eqtr4d	|- ( -. C e. _V -> ( Homf ` C ) = ( x e. B , y e. B |-> ( x H y ) ) )
21	13 20	pm2.61i	|- ( Homf ` C ) = ( x e. B , y e. B |-> ( x H y ) )
22	1 21	eqtri	|- F = ( x e. B , y e. B |-> ( x H y ) )