Definition df-coa 16706

Description: Definition of the composition of arrows. Since arrows are tagged with domain and codomain, this does not need to be a quinary operation like the regular composition in a category comp. Instead, it is a partial binary operation on arrows, which is defined when the domain of the first arrow matches the codomain of the second. (Contributed by Mario Carneiro, 11-Jan-2017.)

Assertion

Ref	Expression
df-coa	|- compa = ( c e. Cat |-> ( g e. (Nat ` c ) , f e. { h e. (Nat ` c ) | (coda ` h ) = (domA ` g ) } |-> <. (domA ` f ) , (coda ` g ) , ( ( 2nd ` g ) ( <. (domA ` f ) , (domA ` g ) >. (comp ` c ) (coda ` g ) ) ( 2nd ` f ) ) >. ) )

Distinct variable group:   f, c, g, h

Detailed syntax breakdown of Definition df-coa

Step	Hyp	Ref	Expression
1		ccoa 16704	. 2 class compa
2		vc	. . 3 setvar c
3		ccat 16325	. . 3 class Cat
4		vg	. . . 4 setvar g
5		vf	. . . 4 setvar f
6	2	cv 1482	. . . . 5 class c
7		carw 16672	. . . . 5 class Nat
8	6, 7	cfv 5888	. . . 4 class (Nat ` c )
9		vh	. . . . . . . 8 setvar h
10	9	cv 1482	. . . . . . 7 class h
11		ccoda 16671	. . . . . . 7 class coda
12	10, 11	cfv 5888	. . . . . 6 class (coda ` h )
13	4	cv 1482	. . . . . . 7 class g
14		cdoma 16670	. . . . . . 7 class domA
15	13, 14	cfv 5888	. . . . . 6 class (domA ` g )
16	12, 15	wceq 1483	. . . . 5 wff (coda ` h ) = (domA ` g )
17	16, 9, 8	crab 2916	. . . 4 class { h e. (Nat ` c ) | (coda ` h ) = (domA ` g ) }
18	5	cv 1482	. . . . . 6 class f
19	18, 14	cfv 5888	. . . . 5 class (domA ` f )
20	13, 11	cfv 5888	. . . . 5 class (coda ` g )
21		c2nd 7167	. . . . . . 7 class 2nd
22	13, 21	cfv 5888	. . . . . 6 class ( 2nd ` g )
23	18, 21	cfv 5888	. . . . . 6 class ( 2nd ` f )
24	19, 15	cop 4183	. . . . . . 7 class <. (domA ` f ) , (domA ` g ) >.
25		cco 15953	. . . . . . . 8 class comp
26	6, 25	cfv 5888	. . . . . . 7 class (comp ` c )
27	24, 20, 26	co 6650	. . . . . 6 class ( <. (domA ` f ) , (domA ` g ) >. (comp ` c ) (coda ` g ) )
28	22, 23, 27	co 6650	. . . . 5 class ( ( 2nd ` g ) ( <. (domA ` f ) , (domA ` g ) >. (comp ` c ) (coda ` g ) ) ( 2nd ` f ) )
29	19, 20, 28	cotp 4185	. . . 4 class <. (domA ` f ) , (coda ` g ) , ( ( 2nd ` g ) ( <. (domA ` f ) , (domA ` g ) >. (comp ` c ) (coda ` g ) ) ( 2nd ` f ) ) >.
30	4, 5, 8, 17, 29	cmpt2 6652	. . 3 class ( g e. (Nat ` c ) , f e. { h e. (Nat ` c ) | (coda ` h ) = (domA ` g ) } |-> <. (domA ` f ) , (coda ` g ) , ( ( 2nd ` g ) ( <. (domA ` f ) , (domA ` g ) >. (comp ` c ) (coda ` g ) ) ( 2nd ` f ) ) >. )
31	2, 3, 30	cmpt 4729	. 2 class ( c e. Cat |-> ( g e. (Nat ` c ) , f e. { h e. (Nat ` c ) | (coda ` h ) = (domA ` g ) } |-> <. (domA ` f ) , (coda ` g ) , ( ( 2nd ` g ) ( <. (domA ` f ) , (domA ` g ) >. (comp ` c ) (coda ` g ) ) ( 2nd ` f ) ) >. ) )
32	1, 31	wceq 1483	1 wff compa = ( c e. Cat |-> ( g e. (Nat ` c ) , f e. { h e. (Nat ` c ) | (coda ` h ) = (domA ` g ) } |-> <. (domA ` f ) , (coda ` g ) , ( ( 2nd ` g ) ( <. (domA ` f ) , (domA ` g ) >. (comp ` c ) (coda ` g ) ) ( 2nd ` f ) ) >. ) )

This definition is referenced by:  coafval  16714