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 5532
Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. For example, ((exp ∘ cos)‘0) = e (ex-co 28227) because (cos‘0) = 1 (see cos0 15499) and (exp‘1) = e (see df-e 15418). 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 5527 . 2 class (𝐴𝐵)
4 vx . . . . . . 7 setvar 𝑥
54cv 1537 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1537 . . . . . 6 class 𝑧
85, 7, 2wbr 5033 . . . . 5 wff 𝑥𝐵𝑧
9 vy . . . . . . 7 setvar 𝑦
109cv 1537 . . . . . 6 class 𝑦
117, 10, 1wbr 5033 . . . . 5 wff 𝑧𝐴𝑦
128, 11wa 399 . . . 4 wff (𝑥𝐵𝑧𝑧𝐴𝑦)
1312, 6wex 1781 . . 3 wff 𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)
1413, 4, 9copab 5095 . 2 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
153, 14wceq 1538 1 wff (𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
Colors of variables: wff setvar class
This definition is referenced by:  coss1  5694  coss2  5695  nfco  5704  brcog  5705  cnvco  5724  cotrg  5942  relco  6068  coundi  6071  coundir  6072  cores  6073  xpco  6112  dffun2  6338  funco  6368  xpcomco  8594  coss12d  14327  xpcogend  14329  trclublem  14350  rtrclreclem3  14415  bj-opabco  34604  bj-xpcossxp  34605  dfcoss3  35821
  Copyright terms: Public domain W3C validator