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 5047
Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. For example, ((exp ∘ cos)‘0) = e (ex-co 26687) because (cos‘0) = 1 (see cos0 14719) and (exp‘1) = e (see df-e 14638). 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 5042 . 2 class (𝐴𝐵)
4 vx . . . . . . 7 setvar 𝑥
54cv 1474 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1474 . . . . . 6 class 𝑧
85, 7, 2wbr 4583 . . . . 5 wff 𝑥𝐵𝑧
9 vy . . . . . . 7 setvar 𝑦
109cv 1474 . . . . . 6 class 𝑦
117, 10, 1wbr 4583 . . . . 5 wff 𝑧𝐴𝑦
128, 11wa 383 . . . 4 wff (𝑥𝐵𝑧𝑧𝐴𝑦)
1312, 6wex 1695 . . 3 wff 𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)
1413, 4, 9copab 4642 . 2 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
153, 14wceq 1475 1 wff (𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
Colors of variables: wff setvar class
This definition is referenced by:  coss1  5199  coss2  5200  nfco  5209  brcog  5210  cnvco  5230  cotrg  5426  relco  5550  coundi  5553  coundir  5554  cores  5555  xpco  5592  dffun2  5814  funco  5842  xpcomco  7935  coss12d  13559  xpcogend  13561  trclublem  13582  rtrclreclem3  13648
  Copyright terms: Public domain W3C validator