Definition df-comf 16332

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.)

Assertion

Ref	Expression
df-comf	|- compf = ( c e. _V |-> ( x e. ( ( Base ` c ) X. ( Base ` c ) ) , y e. ( Base ` c ) |-> ( g e. ( ( 2nd ` x ) ( Hom ` c ) y ) , f e. ( ( Hom ` c ) ` x ) |-> ( g ( x (comp ` c ) y ) f ) ) ) )

Distinct variable group:   f, c, g, x, y

Detailed syntax breakdown of Definition df-comf

Step	Hyp	Ref	Expression
1		ccomf 16328	. 2 class compf
2		vc	. . 3 setvar c
3		cvv 3200	. . 3 class _V
4		vx	. . . 4 setvar x
5		vy	. . . 4 setvar y
6	2	cv 1482	. . . . . 6 class c
7		cbs 15857	. . . . . 6 class Base
8	6, 7	cfv 5888	. . . . 5 class ( Base ` c )
9	8, 8	cxp 5112	. . . 4 class ( ( Base ` c ) X. ( Base ` c ) )
10		vg	. . . . 5 setvar g
11		vf	. . . . 5 setvar f
12	4	cv 1482	. . . . . . 7 class x
13		c2nd 7167	. . . . . . 7 class 2nd
14	12, 13	cfv 5888	. . . . . 6 class ( 2nd ` x )
15	5	cv 1482	. . . . . 6 class y
16		chom 15952	. . . . . . 7 class Hom
17	6, 16	cfv 5888	. . . . . 6 class ( Hom ` c )
18	14, 15, 17	co 6650	. . . . 5 class ( ( 2nd ` x ) ( Hom ` c ) y )
19	12, 17	cfv 5888	. . . . 5 class ( ( Hom ` c ) ` x )
20	10	cv 1482	. . . . . 6 class g
21	11	cv 1482	. . . . . 6 class f
22		cco 15953	. . . . . . . 8 class comp
23	6, 22	cfv 5888	. . . . . . 7 class (comp ` c )
24	12, 15, 23	co 6650	. . . . . 6 class ( x (comp ` c ) y )
25	20, 21, 24	co 6650	. . . . 5 class ( g ( x (comp ` c ) y ) f )
26	10, 11, 18, 19, 25	cmpt2 6652	. . . 4 class ( g e. ( ( 2nd ` x ) ( Hom ` c ) y ) , f e. ( ( Hom ` c ) ` x ) |-> ( g ( x (comp ` c ) y ) f ) )
27	4, 5, 9, 8, 26	cmpt2 6652	. . 3 class ( x e. ( ( Base ` c ) X. ( Base ` c ) ) , y e. ( Base ` c ) |-> ( g e. ( ( 2nd ` x ) ( Hom ` c ) y ) , f e. ( ( Hom ` c ) ` x ) |-> ( g ( x (comp ` c ) y ) f ) ) )
28	2, 3, 27	cmpt 4729	. 2 class ( c e. _V |-> ( x e. ( ( Base ` c ) X. ( Base ` c ) ) , y e. ( Base ` c ) |-> ( g e. ( ( 2nd ` x ) ( Hom ` c ) y ) , f e. ( ( Hom ` c ) ` x ) |-> ( g ( x (comp ` c ) y ) f ) ) ) )
29	1, 28	wceq 1483	1 wff compf = ( c e. _V |-> ( x e. ( ( Base ` c ) X. ( Base ` c ) ) , y e. ( Base ` c ) |-> ( g e. ( ( 2nd ` x ) ( Hom ` c ) y ) , f e. ( ( Hom ` c ) ` x ) |-> ( g ( x (comp ` c ) y ) f ) ) ) )

This definition is referenced by:  comfffval  16358