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 5036
Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. For example, ((exp ∘ cos)‘0) = e (ex-co 26480) because (cos‘0) = 1 (see cos0 14667) and (exp‘1) = e (see df-e 14586). 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 5031 . 2 class (𝐴𝐵)
4 vx . . . . . . 7 setvar 𝑥
54cv 1473 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1473 . . . . . 6 class 𝑧
85, 7, 2wbr 4577 . . . . 5 wff 𝑥𝐵𝑧
9 vy . . . . . . 7 setvar 𝑦
109cv 1473 . . . . . 6 class 𝑦
117, 10, 1wbr 4577 . . . . 5 wff 𝑧𝐴𝑦
128, 11wa 382 . . . 4 wff (𝑥𝐵𝑧𝑧𝐴𝑦)
1312, 6wex 1694 . . 3 wff 𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)
1413, 4, 9copab 4636 . 2 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
153, 14wceq 1474 1 wff (𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
Colors of variables: wff setvar class
This definition is referenced by:  coss1  5186  coss2  5187  nfco  5196  brcog  5197  cnvco  5217  cotrg  5412  relco  5535  coundi  5538  coundir  5539  cores  5540  xpco  5577  dffun2  5799  funco  5827  xpcomco  7912  coss12d  13507  xpcogend  13509  trclublem  13530  rtrclreclem3  13596
  Copyright terms: Public domain W3C validator