Definition df-homf

Description: Define the functionalized Hom-set operator, which is exactly like Hom but is guaranteed to be a function on the base. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Assertion	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)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chomf	$$class{\mathrm{Hom}}_{𝑓}$$
1		vc	$$setvarc$$
2		cvv	$$class\mathrm{V}$$
3		vx	$$setvarx$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarc$$
6	5 4	cfv	$$class{\mathrm{Base}}_c$$
7		vy	$$setvary$$
8	3	cv	$$setvarx$$
9		chom	$$class\mathrm{Hom}$$
10	5 9	cfv	$$class\mathrm{Hom}\left(c\right)$$
11	7	cv	$$setvary$$
12	8 11 10	co	$$class\left(x\mathrm{Hom}\left(c\right)y\right)$$
13	3 7 6 6 12	cmpo	$$class\left(x\in {\mathrm{Base}}_c,y\in {\mathrm{Base}}_c⟼x\mathrm{Hom}\left(c\right)y\right)$$
14	1 2 13	cmpt	$$class\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)$$
15	0 14	wceq	$$wff{\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)$$