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 5416
Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. For example, ((exp ∘ cos)‘0) = e (ex-co 27995) because (cos‘0) = 1 (see cos0 15363) and (exp‘1) = e (see df-e 15282). 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 5411 . 2 class (𝐴𝐵)
4 vx . . . . . . 7 setvar 𝑥
54cv 1506 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1506 . . . . . 6 class 𝑧
85, 7, 2wbr 4929 . . . . 5 wff 𝑥𝐵𝑧
9 vy . . . . . . 7 setvar 𝑦
109cv 1506 . . . . . 6 class 𝑦
117, 10, 1wbr 4929 . . . . 5 wff 𝑧𝐴𝑦
128, 11wa 387 . . . 4 wff (𝑥𝐵𝑧𝑧𝐴𝑦)
1312, 6wex 1742 . . 3 wff 𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)
1413, 4, 9copab 4991 . 2 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
153, 14wceq 1507 1 wff (𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
Colors of variables: wff setvar class
This definition is referenced by:  coss1  5576  coss2  5577  nfco  5586  brcog  5587  cnvco  5606  cotrg  5811  relco  5936  coundi  5939  coundir  5940  cores  5941  xpco  5978  dffun2  6198  funco  6228  xpcomco  8403  coss12d  14193  xpcogend  14195  trclublem  14216  rtrclreclem3  14280  dfcoss3  35113
  Copyright terms: Public domain W3C validator