MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-co Structured version   Visualization version   GIF version

Definition df-co 5694
Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. For example, ((exp ∘ cos)‘0) = e (ex-co 30457) because (cos‘0) = 1 (see cos0 16186) and (exp‘1) = e (see df-e 16104). Note that Definition 7 of [Suppes] p. 63 reverses 𝐴 and 𝐵, uses / instead of , and calls the operation "relative product". (Contributed by NM, 4-Jul-1994.)
Assertion
Ref Expression
df-co (𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑥,𝐵,𝑦,𝑧

Detailed syntax breakdown of Definition df-co
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2ccom 5689 . 2 class (𝐴𝐵)
4 vx . . . . . . 7 setvar 𝑥
54cv 1539 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1539 . . . . . 6 class 𝑧
85, 7, 2wbr 5143 . . . . 5 wff 𝑥𝐵𝑧
9 vy . . . . . . 7 setvar 𝑦
109cv 1539 . . . . . 6 class 𝑦
117, 10, 1wbr 5143 . . . . 5 wff 𝑧𝐴𝑦
128, 11wa 395 . . . 4 wff (𝑥𝐵𝑧𝑧𝐴𝑦)
1312, 6wex 1779 . . 3 wff 𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)
1413, 4, 9copab 5205 . 2 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
153, 14wceq 1540 1 wff (𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
Colors of variables: wff setvar class
This definition is referenced by:  coss1  5866  coss2  5867  nfco  5876  brcog  5877  cnvco  5896  relco  6126  coundi  6267  coundir  6268  cores  6269  xpco  6309  dffun2OLDOLD  6573  funco  6606  xpcomco  9102  coss12d  15011  xpcogend  15013  trclublem  15034  rtrclreclem3  15099  bj-opabco  37189  bj-xpcossxp  37190  dfcoss3  38415
  Copyright terms: Public domain W3C validator