Definition df-coa

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)

	Ref	Expression
Assertion	df-coa	⊢ compa = ( 𝑐 ∈ Cat ↦ ( 𝑔 ∈ ( Arrow ‘ 𝑐 ) , 𝑓 ∈ { ℎ ∈ ( Arrow ‘ 𝑐 ) ∣ ( coda ‘ ℎ ) = ( doma ‘ 𝑔 ) } ↦ ⟨ ( doma ‘ 𝑓 ) , ( coda ‘ 𝑔 ) , ( ( 2nd ‘ 𝑔 ) ( ⟨ ( doma ‘ 𝑓 ) , ( doma ‘ 𝑔 ) ⟩ ( comp ‘ 𝑐 ) ( coda ‘ 𝑔 ) ) ( 2nd ‘ 𝑓 ) ) ⟩ ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccoa	⊢ compa
1		vc	⊢ 𝑐
2		ccat	⊢ Cat
3		vg	⊢ 𝑔
4		carw	⊢ Arrow
5	1	cv	⊢ 𝑐
6	5 4	cfv	⊢ ( Arrow ‘ 𝑐 )
7		vf	⊢ 𝑓
8		vh	⊢ ℎ
9		ccoda	⊢ coda
10	8	cv	⊢ ℎ
11	10 9	cfv	⊢ ( coda ‘ ℎ )
12		cdoma	⊢ doma
13	3	cv	⊢ 𝑔
14	13 12	cfv	⊢ ( doma ‘ 𝑔 )
15	11 14	wceq	⊢ ( coda ‘ ℎ ) = ( doma ‘ 𝑔 )
16	15 8 6	crab	⊢ { ℎ ∈ ( Arrow ‘ 𝑐 ) ∣ ( coda ‘ ℎ ) = ( doma ‘ 𝑔 ) }
17	7	cv	⊢ 𝑓
18	17 12	cfv	⊢ ( doma ‘ 𝑓 )
19	13 9	cfv	⊢ ( coda ‘ 𝑔 )
20		c2nd	⊢ 2nd
21	13 20	cfv	⊢ ( 2nd ‘ 𝑔 )
22	18 14	cop	⊢ ⟨ ( doma ‘ 𝑓 ) , ( doma ‘ 𝑔 ) ⟩
23		cco	⊢ comp
24	5 23	cfv	⊢ ( comp ‘ 𝑐 )
25	22 19 24	co	⊢ ( ⟨ ( doma ‘ 𝑓 ) , ( doma ‘ 𝑔 ) ⟩ ( comp ‘ 𝑐 ) ( coda ‘ 𝑔 ) )
26	17 20	cfv	⊢ ( 2nd ‘ 𝑓 )
27	21 26 25	co	⊢ ( ( 2nd ‘ 𝑔 ) ( ⟨ ( doma ‘ 𝑓 ) , ( doma ‘ 𝑔 ) ⟩ ( comp ‘ 𝑐 ) ( coda ‘ 𝑔 ) ) ( 2nd ‘ 𝑓 ) )
28	18 19 27	cotp	⊢ ⟨ ( doma ‘ 𝑓 ) , ( coda ‘ 𝑔 ) , ( ( 2nd ‘ 𝑔 ) ( ⟨ ( doma ‘ 𝑓 ) , ( doma ‘ 𝑔 ) ⟩ ( comp ‘ 𝑐 ) ( coda ‘ 𝑔 ) ) ( 2nd ‘ 𝑓 ) ) ⟩
29	3 7 6 16 28	cmpo	⊢ ( 𝑔 ∈ ( Arrow ‘ 𝑐 ) , 𝑓 ∈ { ℎ ∈ ( Arrow ‘ 𝑐 ) ∣ ( coda ‘ ℎ ) = ( doma ‘ 𝑔 ) } ↦ ⟨ ( doma ‘ 𝑓 ) , ( coda ‘ 𝑔 ) , ( ( 2nd ‘ 𝑔 ) ( ⟨ ( doma ‘ 𝑓 ) , ( doma ‘ 𝑔 ) ⟩ ( comp ‘ 𝑐 ) ( coda ‘ 𝑔 ) ) ( 2nd ‘ 𝑓 ) ) ⟩ )
30	1 2 29	cmpt	⊢ ( 𝑐 ∈ Cat ↦ ( 𝑔 ∈ ( Arrow ‘ 𝑐 ) , 𝑓 ∈ { ℎ ∈ ( Arrow ‘ 𝑐 ) ∣ ( coda ‘ ℎ ) = ( doma ‘ 𝑔 ) } ↦ ⟨ ( doma ‘ 𝑓 ) , ( coda ‘ 𝑔 ) , ( ( 2nd ‘ 𝑔 ) ( ⟨ ( doma ‘ 𝑓 ) , ( doma ‘ 𝑔 ) ⟩ ( comp ‘ 𝑐 ) ( coda ‘ 𝑔 ) ) ( 2nd ‘ 𝑓 ) ) ⟩ ) )
31	0 30	wceq	⊢ compa = ( 𝑐 ∈ Cat ↦ ( 𝑔 ∈ ( Arrow ‘ 𝑐 ) , 𝑓 ∈ { ℎ ∈ ( Arrow ‘ 𝑐 ) ∣ ( coda ‘ ℎ ) = ( doma ‘ 𝑔 ) } ↦ ⟨ ( doma ‘ 𝑓 ) , ( coda ‘ 𝑔 ) , ( ( 2nd ‘ 𝑔 ) ( ⟨ ( doma ‘ 𝑓 ) , ( doma ‘ 𝑔 ) ⟩ ( comp ‘ 𝑐 ) ( coda ‘ 𝑔 ) ) ( 2nd ‘ 𝑓 ) ) ⟩ ) )