Definition df-cofu 16520

Description: Define the composition of two functors. (Contributed by Mario Carneiro, 3-Jan-2017.)

Assertion

Ref	Expression
df-cofu	|- o.func = ( g e. _V , f e. _V |-> <. ( ( 1st ` g ) o. ( 1st ` f ) ) , ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) >. )

Distinct variable group:   f, g, x, y

Detailed syntax breakdown of Definition df-cofu

Step	Hyp	Ref	Expression
1		ccofu 16516	. 2 class o.func
2		vg	. . 3 setvar g
3		vf	. . 3 setvar f
4		cvv 3200	. . 3 class _V
5	2	cv 1482	. . . . . 6 class g
6		c1st 7166	. . . . . 6 class 1st
7	5, 6	cfv 5888	. . . . 5 class ( 1st ` g )
8	3	cv 1482	. . . . . 6 class f
9	8, 6	cfv 5888	. . . . 5 class ( 1st ` f )
10	7, 9	ccom 5118	. . . 4 class ( ( 1st ` g ) o. ( 1st ` f ) )
11		vx	. . . . 5 setvar x
12		vy	. . . . 5 setvar y
13		c2nd 7167	. . . . . . . 8 class 2nd
14	8, 13	cfv 5888	. . . . . . 7 class ( 2nd ` f )
15	14	cdm 5114	. . . . . 6 class dom ( 2nd ` f )
16	15	cdm 5114	. . . . 5 class dom dom ( 2nd ` f )
17	11	cv 1482	. . . . . . . 8 class x
18	17, 9	cfv 5888	. . . . . . 7 class ( ( 1st ` f ) ` x )
19	12	cv 1482	. . . . . . . 8 class y
20	19, 9	cfv 5888	. . . . . . 7 class ( ( 1st ` f ) ` y )
21	5, 13	cfv 5888	. . . . . . 7 class ( 2nd ` g )
22	18, 20, 21	co 6650	. . . . . 6 class ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) )
23	17, 19, 14	co 6650	. . . . . 6 class ( x ( 2nd ` f ) y )
24	22, 23	ccom 5118	. . . . 5 class ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) )
25	11, 12, 16, 16, 24	cmpt2 6652	. . . 4 class ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) )
26	10, 25	cop 4183	. . 3 class <. ( ( 1st ` g ) o. ( 1st ` f ) ) , ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) >.
27	2, 3, 4, 4, 26	cmpt2 6652	. 2 class ( g e. _V , f e. _V |-> <. ( ( 1st ` g ) o. ( 1st ` f ) ) , ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) >. )
28	1, 27	wceq 1483	1 wff o.func = ( g e. _V , f e. _V |-> <. ( ( 1st ` g ) o. ( 1st ` f ) ) , ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) >. )

This definition is referenced by:  cofuval  16542