Metamath Proof Explorer

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 ⊢ comp a = c ∈ Cat ⟼ g ∈ Arrow ⁡ c , f ∈ h ∈ Arrow ⁡ c | cod a ⁡ h = dom a ⁡ g ⟼ dom a ⁡ f cod a ⁡ g 2 nd ⁡ g dom a ⁡ f dom a ⁡ g comp ⁡ c cod a ⁡ g 2 nd ⁡ f

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccoa class comp a
1 vc setvar c
2 ccat class Cat
3 vg setvar g
4 carw class Arrow
5 1 cv setvar c
6 5 4 cfv class Arrow ⁡ c
7 vf setvar f
8 vh setvar h
9 ccoda class cod a
10 8 cv setvar h
11 10 9 cfv class cod a ⁡ h
12 cdoma class dom a
13 3 cv setvar g
14 13 12 cfv class dom a ⁡ g
15 11 14 wceq wff cod a ⁡ h = dom a ⁡ g
16 15 8 6 crab class h ∈ Arrow ⁡ c | cod a ⁡ h = dom a ⁡ g
17 7 cv setvar f
18 17 12 cfv class dom a ⁡ f
19 13 9 cfv class cod a ⁡ g
20 c2nd class 2 nd
21 13 20 cfv class 2 nd ⁡ g
22 18 14 cop class dom a ⁡ f dom a ⁡ g
23 cco class comp
24 5 23 cfv class comp ⁡ c
25 22 19 24 co class dom a ⁡ f dom a ⁡ g comp ⁡ c cod a ⁡ g
26 17 20 cfv class 2 nd ⁡ f
27 21 26 25 co class 2 nd ⁡ g dom a ⁡ f dom a ⁡ g comp ⁡ c cod a ⁡ g 2 nd ⁡ f
28 18 19 27 cotp class dom a ⁡ f cod a ⁡ g 2 nd ⁡ g dom a ⁡ f dom a ⁡ g comp ⁡ c cod a ⁡ g 2 nd ⁡ f
29 3 7 6 16 28 cmpo class g ∈ Arrow ⁡ c , f ∈ h ∈ Arrow ⁡ c | cod a ⁡ h = dom a ⁡ g ⟼ dom a ⁡ f cod a ⁡ g 2 nd ⁡ g dom a ⁡ f dom a ⁡ g comp ⁡ c cod a ⁡ g 2 nd ⁡ f
30 1 2 29 cmpt class c ∈ Cat ⟼ g ∈ Arrow ⁡ c , f ∈ h ∈ Arrow ⁡ c | cod a ⁡ h = dom a ⁡ g ⟼ dom a ⁡ f cod a ⁡ g 2 nd ⁡ g dom a ⁡ f dom a ⁡ g comp ⁡ c cod a ⁡ g 2 nd ⁡ f
31 0 30 wceq wff comp a = c ∈ Cat ⟼ g ∈ Arrow ⁡ c , f ∈ h ∈ Arrow ⁡ c | cod a ⁡ h = dom a ⁡ g ⟼ dom a ⁡ f cod a ⁡ g 2 nd ⁡ g dom a ⁡ f dom a ⁡ g comp ⁡ c cod a ⁡ g 2 nd ⁡ f