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={\mathrm{Hom}}_{𝑓}\left(C\right)$$
	homffval.b	$$⊢B={\mathrm{Base}}_C$$
	homffval.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
Assertion	homffval	$$⊢F=\left(x\in B,y\in B⟼xHy\right)$$

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		fveq2	$$⊢c=C\to {\mathrm{Base}}_c={\mathrm{Base}}_C$$
5	4 2	eqtr4di	$$⊢c=C\to {\mathrm{Base}}_c=B$$
6		fveq2	$$⊢c=C\to \mathrm{Hom}\left(c\right)=\mathrm{Hom}\left(C\right)$$
7	6 3	eqtr4di	$$⊢c=C\to \mathrm{Hom}\left(c\right)=H$$
8	7	oveqd	$$⊢c=C\to x\mathrm{Hom}\left(c\right)y=xHy$$
9	5 5 8	mpoeq123dv	$$⊢c=C\to \left(x\in {\mathrm{Base}}_c,y\in {\mathrm{Base}}_c⟼x\mathrm{Hom}\left(c\right)y\right)=\left(x\in B,y\in B⟼xHy\right)$$
10		df-homf	$$⊢{\mathrm{Hom}}_{𝑓}=\left(c\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_c,y\in {\mathrm{Base}}_c⟼x\mathrm{Hom}\left(c\right)y\right)\right)$$
11	2	fvexi	$$⊢B\in \mathrm{V}$$
12	11 11	mpoex	$$⊢\left(x\in B,y\in B⟼xHy\right)\in \mathrm{V}$$
13	9 10 12	fvmpt	$$⊢C\in \mathrm{V}\to {\mathrm{Hom}}_{𝑓}\left(C\right)=\left(x\in B,y\in B⟼xHy\right)$$
14		fvprc	$$⊢\neg C\in \mathrm{V}\to {\mathrm{Hom}}_{𝑓}\left(C\right)=\varnothing$$
15		fvprc	$$⊢\neg C\in \mathrm{V}\to {\mathrm{Base}}_C=\varnothing$$
16	2 15	eqtrid	$$⊢\neg C\in \mathrm{V}\to B=\varnothing$$
17	16	olcd	$$⊢\neg C\in \mathrm{V}\to \left(B=\varnothing \vee B=\varnothing \right)$$
18		0mpo0	$$⊢\left(B=\varnothing \vee B=\varnothing \right)\to \left(x\in B,y\in B⟼xHy\right)=\varnothing$$
19	17 18	syl	$$⊢\neg C\in \mathrm{V}\to \left(x\in B,y\in B⟼xHy\right)=\varnothing$$
20	14 19	eqtr4d	$$⊢\neg C\in \mathrm{V}\to {\mathrm{Hom}}_{𝑓}\left(C\right)=\left(x\in B,y\in B⟼xHy\right)$$
21	13 20	pm2.61i	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)=\left(x\in B,y\in B⟼xHy\right)$$
22	1 21	eqtri	$$⊢F=\left(x\in B,y\in B⟼xHy\right)$$