Definition df-coa 17771

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 = (𝑐 ∈ Cat ↦ (𝑔 ∈ (Arrow‘𝑐), 𝑓 ∈ {ℎ ∈ (Arrow‘𝑐) ∣ (coda‘ℎ) = (doma‘𝑔)} ↦ ⟨(doma‘𝑓), (coda‘𝑔), ((2nd ‘𝑔)(⟨(doma‘𝑓), (doma‘𝑔)⟩(comp‘𝑐)(coda‘𝑔))(2nd ‘𝑓))⟩))

Distinct variable group:   𝑓,𝑐,𝑔,ℎ

Detailed syntax breakdown of Definition df-coa

Step	Hyp	Ref	Expression
1		ccoa 17769	. 2 class compa
2		vc	. . 3 setvar 𝑐
3		ccat 17373	. . 3 class Cat
4		vg	. . . 4 setvar 𝑔
5		vf	. . . 4 setvar 𝑓
6	2	cv 1538	. . . . 5 class 𝑐
7		carw 17737	. . . . 5 class Arrow
8	6, 7	cfv 6433	. . . 4 class (Arrow‘𝑐)
9		vh	. . . . . . . 8 setvar ℎ
10	9	cv 1538	. . . . . . 7 class ℎ
11		ccoda 17736	. . . . . . 7 class coda
12	10, 11	cfv 6433	. . . . . 6 class (coda‘ℎ)
13	4	cv 1538	. . . . . . 7 class 𝑔
14		cdoma 17735	. . . . . . 7 class doma
15	13, 14	cfv 6433	. . . . . 6 class (doma‘𝑔)
16	12, 15	wceq 1539	. . . . 5 wff (coda‘ℎ) = (doma‘𝑔)
17	16, 9, 8	crab 3068	. . . 4 class {ℎ ∈ (Arrow‘𝑐) ∣ (coda‘ℎ) = (doma‘𝑔)}
18	5	cv 1538	. . . . . 6 class 𝑓
19	18, 14	cfv 6433	. . . . 5 class (doma‘𝑓)
20	13, 11	cfv 6433	. . . . 5 class (coda‘𝑔)
21		c2nd 7830	. . . . . . 7 class 2nd
22	13, 21	cfv 6433	. . . . . 6 class (2nd ‘𝑔)
23	18, 21	cfv 6433	. . . . . 6 class (2nd ‘𝑓)
24	19, 15	cop 4567	. . . . . . 7 class ⟨(doma‘𝑓), (doma‘𝑔)⟩
25		cco 16974	. . . . . . . 8 class comp
26	6, 25	cfv 6433	. . . . . . 7 class (comp‘𝑐)
27	24, 20, 26	co 7275	. . . . . 6 class (⟨(doma‘𝑓), (doma‘𝑔)⟩(comp‘𝑐)(coda‘𝑔))
28	22, 23, 27	co 7275	. . . . 5 class ((2nd ‘𝑔)(⟨(doma‘𝑓), (doma‘𝑔)⟩(comp‘𝑐)(coda‘𝑔))(2nd ‘𝑓))
29	19, 20, 28	cotp 4569	. . . 4 class ⟨(doma‘𝑓), (coda‘𝑔), ((2nd ‘𝑔)(⟨(doma‘𝑓), (doma‘𝑔)⟩(comp‘𝑐)(coda‘𝑔))(2nd ‘𝑓))⟩
30	4, 5, 8, 17, 29	cmpo 7277	. . 3 class (𝑔 ∈ (Arrow‘𝑐), 𝑓 ∈ {ℎ ∈ (Arrow‘𝑐) ∣ (coda‘ℎ) = (doma‘𝑔)} ↦ ⟨(doma‘𝑓), (coda‘𝑔), ((2nd ‘𝑔)(⟨(doma‘𝑓), (doma‘𝑔)⟩(comp‘𝑐)(coda‘𝑔))(2nd ‘𝑓))⟩)
31	2, 3, 30	cmpt 5157	. 2 class (𝑐 ∈ Cat ↦ (𝑔 ∈ (Arrow‘𝑐), 𝑓 ∈ {ℎ ∈ (Arrow‘𝑐) ∣ (coda‘ℎ) = (doma‘𝑔)} ↦ ⟨(doma‘𝑓), (coda‘𝑔), ((2nd ‘𝑔)(⟨(doma‘𝑓), (doma‘𝑔)⟩(comp‘𝑐)(coda‘𝑔))(2nd ‘𝑓))⟩))
32	1, 31	wceq 1539	1 wff compa = (𝑐 ∈ Cat ↦ (𝑔 ∈ (Arrow‘𝑐), 𝑓 ∈ {ℎ ∈ (Arrow‘𝑐) ∣ (coda‘ℎ) = (doma‘𝑔)} ↦ ⟨(doma‘𝑓), (coda‘𝑔), ((2nd ‘𝑔)(⟨(doma‘𝑓), (doma‘𝑔)⟩(comp‘𝑐)(coda‘𝑔))(2nd ‘𝑓))⟩))

This definition is referenced by:  coafval  17779