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 5697
Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. For example, ((exp ∘ cos)‘0) = e (ex-co 30466) because (cos‘0) = 1 (see cos0 16182) and (exp‘1) = e (see df-e 16100). 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 5692 . 2 class (𝐴𝐵)
4 vx . . . . . . 7 setvar 𝑥
54cv 1535 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1535 . . . . . 6 class 𝑧
85, 7, 2wbr 5147 . . . . 5 wff 𝑥𝐵𝑧
9 vy . . . . . . 7 setvar 𝑦
109cv 1535 . . . . . 6 class 𝑦
117, 10, 1wbr 5147 . . . . 5 wff 𝑧𝐴𝑦
128, 11wa 395 . . . 4 wff (𝑥𝐵𝑧𝑧𝐴𝑦)
1312, 6wex 1775 . . 3 wff 𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)
1413, 4, 9copab 5209 . 2 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
153, 14wceq 1536 1 wff (𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
Colors of variables: wff setvar class
This definition is referenced by:  coss1  5868  coss2  5869  nfco  5878  brcog  5879  cnvco  5898  relco  6128  coundi  6268  coundir  6269  cores  6270  xpco  6310  dffun2OLDOLD  6574  funco  6607  xpcomco  9100  coss12d  15007  xpcogend  15009  trclublem  15030  rtrclreclem3  15095  bj-opabco  37170  bj-xpcossxp  37171  dfcoss3  38395
  Copyright terms: Public domain W3C validator