MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-coa Structured version   Visualization version   GIF version
Definition df-coa 18006
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
StepHypRef Expression
1 ccoa 18004 . 2 class compa
2 vc . . 3 setvar 𝑐
3 ccat 17608 . . 3 class Cat
4 vg . . . 4 setvar 𝑔
5 vf . . . 4 setvar 𝑓
62cv 1541 . . . . 5 class 𝑐
7 carw 17972 . . . . 5 class Arrow
86, 7cfv 6544 . . . 4 class (Arrowβ€˜π‘)
9 vh . . . . . . . 8 setvar β„Ž
109cv 1541 . . . . . . 7 class β„Ž
11 ccoda 17971 . . . . . . 7 class coda
1210, 11cfv 6544 . . . . . 6 class (codaβ€˜β„Ž)
134cv 1541 . . . . . . 7 class 𝑔
14 cdoma 17970 . . . . . . 7 class doma
1513, 14cfv 6544 . . . . . 6 class (domaβ€˜π‘”)
1612, 15wceq 1542 . . . . 5 wff (codaβ€˜β„Ž) = (domaβ€˜π‘”)
1716, 9, 8crab 3433 . . . 4 class {β„Ž ∈ (Arrowβ€˜π‘) ∣ (codaβ€˜β„Ž) = (domaβ€˜π‘”)}
185cv 1541 . . . . . 6 class 𝑓
1918, 14cfv 6544 . . . . 5 class (domaβ€˜π‘“)
2013, 11cfv 6544 . . . . 5 class (codaβ€˜π‘”)
21 c2nd 7974 . . . . . . 7 class 2nd
2213, 21cfv 6544 . . . . . 6 class (2nd β€˜π‘”)
2318, 21cfv 6544 . . . . . 6 class (2nd β€˜π‘“)
2419, 15cop 4635 . . . . . . 7 class ⟨(domaβ€˜π‘“), (domaβ€˜π‘”)⟩
25 cco 17209 . . . . . . . 8 class comp
266, 25cfv 6544 . . . . . . 7 class (compβ€˜π‘)
2724, 20, 26co 7409 . . . . . 6 class (⟨(domaβ€˜π‘“), (domaβ€˜π‘”)⟩(compβ€˜π‘)(codaβ€˜π‘”))
2822, 23, 27co 7409 . . . . 5 class ((2nd β€˜π‘”)(⟨(domaβ€˜π‘“), (domaβ€˜π‘”)⟩(compβ€˜π‘)(codaβ€˜π‘”))(2nd β€˜π‘“))
2919, 20, 28cotp 4637 . . . 4 class ⟨(domaβ€˜π‘“), (codaβ€˜π‘”), ((2nd β€˜π‘”)(⟨(domaβ€˜π‘“), (domaβ€˜π‘”)⟩(compβ€˜π‘)(codaβ€˜π‘”))(2nd β€˜π‘“))⟩
304, 5, 8, 17, 29cmpo 7411 . . 3 class (𝑔 ∈ (Arrowβ€˜π‘), 𝑓 ∈ {β„Ž ∈ (Arrowβ€˜π‘) ∣ (codaβ€˜β„Ž) = (domaβ€˜π‘”)} ↦ ⟨(domaβ€˜π‘“), (codaβ€˜π‘”), ((2nd β€˜π‘”)(⟨(domaβ€˜π‘“), (domaβ€˜π‘”)⟩(compβ€˜π‘)(codaβ€˜π‘”))(2nd β€˜π‘“))⟩)
312, 3, 30cmpt 5232 . 2 class (𝑐 ∈ Cat ↦ (𝑔 ∈ (Arrowβ€˜π‘), 𝑓 ∈ {β„Ž ∈ (Arrowβ€˜π‘) ∣ (codaβ€˜β„Ž) = (domaβ€˜π‘”)} ↦ ⟨(domaβ€˜π‘“), (codaβ€˜π‘”), ((2nd β€˜π‘”)(⟨(domaβ€˜π‘“), (domaβ€˜π‘”)⟩(compβ€˜π‘)(codaβ€˜π‘”))(2nd β€˜π‘“))⟩))
321, 31wceq 1542 1 wff compa = (𝑐 ∈ Cat ↦ (𝑔 ∈ (Arrowβ€˜π‘), 𝑓 ∈ {β„Ž ∈ (Arrowβ€˜π‘) ∣ (codaβ€˜β„Ž) = (domaβ€˜π‘”)} ↦ ⟨(domaβ€˜π‘“), (codaβ€˜π‘”), ((2nd β€˜π‘”)(⟨(domaβ€˜π‘“), (domaβ€˜π‘”)⟩(compβ€˜π‘)(codaβ€˜π‘”))(2nd β€˜π‘“))⟩))
Colors of variables: wff setvar class
This definition is referenced by:  coafval  18014
  Copyright terms: Public domain W3C validator