Theorem homfval

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

	Ref	Expression
Hypotheses	homffval.f	$$⊢F={\mathrm{Hom}}_{𝑓}\left(C\right)$$
	homffval.b	$$⊢B={\mathrm{Base}}_C$$
	homffval.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	homfval.x	$$⊢\phi \to X\in B$$
	homfval.y	$$⊢\phi \to Y\in B$$
Assertion	homfval	$$⊢\phi \to XFY=XHY$$

Proof

Step	Hyp	Ref	Expression
1		homffval.f	$$⊢F={\mathrm{Hom}}_{𝑓}\left(C\right)$$
2		homffval.b	$$⊢B={\mathrm{Base}}_C$$
3		homffval.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
4		homfval.x	$$⊢\phi \to X\in B$$
5		homfval.y	$$⊢\phi \to Y\in B$$
6	1 2 3	homffval	$$⊢F=\left(x\in B,y\in B⟼xHy\right)$$
7	6	a1i	$$⊢\phi \to F=\left(x\in B,y\in B⟼xHy\right)$$
8		oveq12	$$⊢\left(x=X\wedge y=Y\right)\to xHy=XHY$$
9	8	adantl	$$⊢\left(\phi \wedge \left(x=X\wedge y=Y\right)\right)\to xHy=XHY$$
10		ovexd	$$⊢\phi \to XHY\in \mathrm{V}$$
11	7 9 4 5 10	ovmpod	$$⊢\phi \to XFY=XHY$$