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 5093
Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. For example, ((exp ∘ cos)‘0) = e (ex-co 27183) because (cos‘0) = 1 (see cos0 14824) and (exp‘1) = e (see df-e 14743). 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 5088 . 2 class (𝐴𝐵)
4 vx . . . . . . 7 setvar 𝑥
54cv 1479 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1479 . . . . . 6 class 𝑧
85, 7, 2wbr 4623 . . . . 5 wff 𝑥𝐵𝑧
9 vy . . . . . . 7 setvar 𝑦
109cv 1479 . . . . . 6 class 𝑦
117, 10, 1wbr 4623 . . . . 5 wff 𝑧𝐴𝑦
128, 11wa 384 . . . 4 wff (𝑥𝐵𝑧𝑧𝐴𝑦)
1312, 6wex 1701 . . 3 wff 𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)
1413, 4, 9copab 4682 . 2 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
153, 14wceq 1480 1 wff (𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
Colors of variables: wff setvar class
This definition is referenced by:  coss1  5247  coss2  5248  nfco  5257  brcog  5258  cnvco  5278  cotrg  5476  relco  5602  coundi  5605  coundir  5606  cores  5607  xpco  5644  dffun2  5867  funco  5896  xpcomco  8010  coss12d  13661  xpcogend  13663  trclublem  13684  rtrclreclem3  13750
  Copyright terms: Public domain W3C validator