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 16475
Description: Definition of the composition of arrows. Since arrows are tagged with domain and codomain, this does not need to be a 5-ary 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 16473 . 2 class compa
2 vc . . 3 setvar 𝑐
3 ccat 16094 . . 3 class Cat
4 vg . . . 4 setvar 𝑔
5 vf . . . 4 setvar 𝑓
62cv 1473 . . . . 5 class 𝑐
7 carw 16441 . . . . 5 class Arrow
86, 7cfv 5790 . . . 4 class (Arrow‘𝑐)
9 vh . . . . . . . 8 setvar
109cv 1473 . . . . . . 7 class
11 ccoda 16440 . . . . . . 7 class coda
1210, 11cfv 5790 . . . . . 6 class (coda)
134cv 1473 . . . . . . 7 class 𝑔
14 cdoma 16439 . . . . . . 7 class doma
1513, 14cfv 5790 . . . . . 6 class (doma𝑔)
1612, 15wceq 1474 . . . . 5 wff (coda) = (doma𝑔)
1716, 9, 8crab 2899 . . . 4 class { ∈ (Arrow‘𝑐) ∣ (coda) = (doma𝑔)}
185cv 1473 . . . . . 6 class 𝑓
1918, 14cfv 5790 . . . . 5 class (doma𝑓)
2013, 11cfv 5790 . . . . 5 class (coda𝑔)
21 c2nd 7035 . . . . . . 7 class 2nd
2213, 21cfv 5790 . . . . . 6 class (2nd𝑔)
2318, 21cfv 5790 . . . . . 6 class (2nd𝑓)
2419, 15cop 4130 . . . . . . 7 class ⟨(doma𝑓), (doma𝑔)⟩
25 cco 15726 . . . . . . . 8 class comp
266, 25cfv 5790 . . . . . . 7 class (comp‘𝑐)
2724, 20, 26co 6527 . . . . . 6 class (⟨(doma𝑓), (doma𝑔)⟩(comp‘𝑐)(coda𝑔))
2822, 23, 27co 6527 . . . . 5 class ((2nd𝑔)(⟨(doma𝑓), (doma𝑔)⟩(comp‘𝑐)(coda𝑔))(2nd𝑓))
2919, 20, 28cotp 4132 . . . 4 class ⟨(doma𝑓), (coda𝑔), ((2nd𝑔)(⟨(doma𝑓), (doma𝑔)⟩(comp‘𝑐)(coda𝑔))(2nd𝑓))⟩
304, 5, 8, 17, 29cmpt2 6529 . . 3 class (𝑔 ∈ (Arrow‘𝑐), 𝑓 ∈ { ∈ (Arrow‘𝑐) ∣ (coda) = (doma𝑔)} ↦ ⟨(doma𝑓), (coda𝑔), ((2nd𝑔)(⟨(doma𝑓), (doma𝑔)⟩(comp‘𝑐)(coda𝑔))(2nd𝑓))⟩)
312, 3, 30cmpt 4637 . 2 class (𝑐 ∈ Cat ↦ (𝑔 ∈ (Arrow‘𝑐), 𝑓 ∈ { ∈ (Arrow‘𝑐) ∣ (coda) = (doma𝑔)} ↦ ⟨(doma𝑓), (coda𝑔), ((2nd𝑔)(⟨(doma𝑓), (doma𝑔)⟩(comp‘𝑐)(coda𝑔))(2nd𝑓))⟩))
321, 31wceq 1474 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  16483
  Copyright terms: Public domain W3C validator