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 5152
Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. For example, ((exp ∘ cos)‘0) = e (ex-co 27425) because (cos‘0) = 1 (see cos0 14924) and (exp‘1) = e (see df-e 14843). 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 5147 . 2 class (𝐴𝐵)
4 vx . . . . . . 7 setvar 𝑥
54cv 1522 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1522 . . . . . 6 class 𝑧
85, 7, 2wbr 4685 . . . . 5 wff 𝑥𝐵𝑧
9 vy . . . . . . 7 setvar 𝑦
109cv 1522 . . . . . 6 class 𝑦
117, 10, 1wbr 4685 . . . . 5 wff 𝑧𝐴𝑦
128, 11wa 383 . . . 4 wff (𝑥𝐵𝑧𝑧𝐴𝑦)
1312, 6wex 1744 . . 3 wff 𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)
1413, 4, 9copab 4745 . 2 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
153, 14wceq 1523 1 wff (𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
Colors of variables: wff setvar class
This definition is referenced by:  coss1  5310  coss2  5311  nfco  5320  brcog  5321  cnvco  5340  cotrg  5542  relco  5671  coundi  5674  coundir  5675  cores  5676  xpco  5713  dffun2  5936  funco  5966  xpcomco  8091  coss12d  13757  xpcogend  13759  trclublem  13780  rtrclreclem3  13844  dfcoss3  34312
  Copyright terms: Public domain W3C validator