Definition df-comf

Description: Define the functionalized composition operator, which is exactly like comp but is guaranteed to be a function of the proper type. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Assertion	df-comf	$$⊢{\mathrm{comp}}_{𝑓}=\left(c\in \mathrm{V}⟼\left(x\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_c\right),y\in {\mathrm{Base}}_c⟼\left(g\in \left(2^{nd}\left(x\right)\mathrm{Hom}\left(c\right)y\right),f\in \mathrm{Hom}\left(c\right)\left(x\right)⟼g\left(x\mathrm{comp}\left(c\right)y\right)f\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccomf	$$class{\mathrm{comp}}_{𝑓}$$
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	6 6	cxp	$$class\left({\mathrm{Base}}_c\times {\mathrm{Base}}_c\right)$$
8		vy	$$setvary$$
9		vg	$$setvarg$$
10		c2nd	$$class{2}^{nd}$$
11	3	cv	$$setvarx$$
12	11 10	cfv	$$class{2}^{nd}\left(x\right)$$
13		chom	$$class\mathrm{Hom}$$
14	5 13	cfv	$$class\mathrm{Hom}\left(c\right)$$
15	8	cv	$$setvary$$
16	12 15 14	co	$$class\left(2^{nd}\left(x\right)\mathrm{Hom}\left(c\right)y\right)$$
17		vf	$$setvarf$$
18	11 14	cfv	$$class\mathrm{Hom}\left(c\right)\left(x\right)$$
19	9	cv	$$setvarg$$
20		cco	$$class\mathrm{comp}$$
21	5 20	cfv	$$class\mathrm{comp}\left(c\right)$$
22	11 15 21	co	$$class\left(x\mathrm{comp}\left(c\right)y\right)$$
23	17	cv	$$setvarf$$
24	19 23 22	co	$$class\left(g\left(x\mathrm{comp}\left(c\right)y\right)f\right)$$
25	9 17 16 18 24	cmpo	$$class\left(g\in \left(2^{nd}\left(x\right)\mathrm{Hom}\left(c\right)y\right),f\in \mathrm{Hom}\left(c\right)\left(x\right)⟼g\left(x\mathrm{comp}\left(c\right)y\right)f\right)$$
26	3 8 7 6 25	cmpo	$$class\left(x\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_c\right),y\in {\mathrm{Base}}_c⟼\left(g\in \left(2^{nd}\left(x\right)\mathrm{Hom}\left(c\right)y\right),f\in \mathrm{Hom}\left(c\right)\left(x\right)⟼g\left(x\mathrm{comp}\left(c\right)y\right)f\right)\right)$$
27	1 2 26	cmpt	$$class\left(c\in \mathrm{V}⟼\left(x\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_c\right),y\in {\mathrm{Base}}_c⟼\left(g\in \left(2^{nd}\left(x\right)\mathrm{Hom}\left(c\right)y\right),f\in \mathrm{Hom}\left(c\right)\left(x\right)⟼g\left(x\mathrm{comp}\left(c\right)y\right)f\right)\right)\right)$$
28	0 27	wceq	$$wff{\mathrm{comp}}_{𝑓}=\left(c\in \mathrm{V}⟼\left(x\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_c\right),y\in {\mathrm{Base}}_c⟼\left(g\in \left(2^{nd}\left(x\right)\mathrm{Hom}\left(c\right)y\right),f\in \mathrm{Hom}\left(c\right)\left(x\right)⟼g\left(x\mathrm{comp}\left(c\right)y\right)f\right)\right)\right)$$