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 16912
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 16910 . 2 class compa
2 vc . . 3 setvar 𝑐
3 ccat 16531 . . 3 class Cat
4 vg . . . 4 setvar 𝑔
5 vf . . . 4 setvar 𝑓
62cv 1629 . . . . 5 class 𝑐
7 carw 16878 . . . . 5 class Arrow
86, 7cfv 6031 . . . 4 class (Arrow‘𝑐)
9 vh . . . . . . . 8 setvar
109cv 1629 . . . . . . 7 class
11 ccoda 16877 . . . . . . 7 class coda
1210, 11cfv 6031 . . . . . 6 class (coda)
134cv 1629 . . . . . . 7 class 𝑔
14 cdoma 16876 . . . . . . 7 class doma
1513, 14cfv 6031 . . . . . 6 class (doma𝑔)
1612, 15wceq 1630 . . . . 5 wff (coda) = (doma𝑔)
1716, 9, 8crab 3064 . . . 4 class { ∈ (Arrow‘𝑐) ∣ (coda) = (doma𝑔)}
185cv 1629 . . . . . 6 class 𝑓
1918, 14cfv 6031 . . . . 5 class (doma𝑓)
2013, 11cfv 6031 . . . . 5 class (coda𝑔)
21 c2nd 7313 . . . . . . 7 class 2nd
2213, 21cfv 6031 . . . . . 6 class (2nd𝑔)
2318, 21cfv 6031 . . . . . 6 class (2nd𝑓)
2419, 15cop 4320 . . . . . . 7 class ⟨(doma𝑓), (doma𝑔)⟩
25 cco 16160 . . . . . . . 8 class comp
266, 25cfv 6031 . . . . . . 7 class (comp‘𝑐)
2724, 20, 26co 6792 . . . . . 6 class (⟨(doma𝑓), (doma𝑔)⟩(comp‘𝑐)(coda𝑔))
2822, 23, 27co 6792 . . . . 5 class ((2nd𝑔)(⟨(doma𝑓), (doma𝑔)⟩(comp‘𝑐)(coda𝑔))(2nd𝑓))
2919, 20, 28cotp 4322 . . . 4 class ⟨(doma𝑓), (coda𝑔), ((2nd𝑔)(⟨(doma𝑓), (doma𝑔)⟩(comp‘𝑐)(coda𝑔))(2nd𝑓))⟩
304, 5, 8, 17, 29cmpt2 6794 . . 3 class (𝑔 ∈ (Arrow‘𝑐), 𝑓 ∈ { ∈ (Arrow‘𝑐) ∣ (coda) = (doma𝑔)} ↦ ⟨(doma𝑓), (coda𝑔), ((2nd𝑔)(⟨(doma𝑓), (doma𝑔)⟩(comp‘𝑐)(coda𝑔))(2nd𝑓))⟩)
312, 3, 30cmpt 4861 . 2 class (𝑐 ∈ Cat ↦ (𝑔 ∈ (Arrow‘𝑐), 𝑓 ∈ { ∈ (Arrow‘𝑐) ∣ (coda) = (doma𝑔)} ↦ ⟨(doma𝑓), (coda𝑔), ((2nd𝑔)(⟨(doma𝑓), (doma𝑔)⟩(comp‘𝑐)(coda𝑔))(2nd𝑓))⟩))
321, 31wceq 1630 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  16920
  Copyright terms: Public domain W3C validator