Theorem fnhomeqhomf

Description: If the Hom-set operation is a function it is equal to the corresponding functionalized Hom-set operation. (Contributed by AV, 1-Mar-2020)

	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	fnhomeqhomf	$$⊢HFn\left(B\times B\right)\to F=H$$

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		fnov	$$⊢HFn\left(B\times B\right)\leftrightarrow H=\left(x\in B,y\in B⟼xHy\right)$$
5	1 2 3	homffval	$$⊢F=\left(x\in B,y\in B⟼xHy\right)$$
6		eqeq2	$$⊢H=\left(x\in B,y\in B⟼xHy\right)\to \left(F=H\leftrightarrow F=\left(x\in B,y\in B⟼xHy\right)\right)$$
7	5 6	mpbiri	$$⊢H=\left(x\in B,y\in B⟼xHy\right)\to F=H$$
8	4 7	sylbi	$$⊢HFn\left(B\times B\right)\to F=H$$