Theorem homffn

Description: The functionalized Hom-set operation is a function. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Hypotheses	homffn.f	$$⊢F={\mathrm{Hom}}_{𝑓}\left(C\right)$$
	homffn.b	$$⊢B={\mathrm{Base}}_C$$
Assertion	homffn	$$⊢FFn\left(B\times B\right)$$

Proof

Step	Hyp	Ref	Expression
1		homffn.f	$$⊢F={\mathrm{Hom}}_{𝑓}\left(C\right)$$
2		homffn.b	$$⊢B={\mathrm{Base}}_C$$
3		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
4	1 2 3	homffval	$$⊢F=\left(x\in B,y\in B⟼x\mathrm{Hom}\left(C\right)y\right)$$
5		ovex	$$⊢x\mathrm{Hom}\left(C\right)y\in \mathrm{V}$$
6	4 5	fnmpoi	$$⊢FFn\left(B\times B\right)$$