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 5320
Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. For example, ((exp ∘ cos)‘0) = e (ex-co 27622) because (cos‘0) = 1 (see cos0 15096) and (exp‘1) = e (see df-e 15015). 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 5315 . 2 class (𝐴𝐵)
4 vx . . . . . . 7 setvar 𝑥
54cv 1636 . . . . . 6 class 𝑥
6 vz . . . . . . 7 setvar 𝑧
76cv 1636 . . . . . 6 class 𝑧
85, 7, 2wbr 4844 . . . . 5 wff 𝑥𝐵𝑧
9 vy . . . . . . 7 setvar 𝑦
109cv 1636 . . . . . 6 class 𝑦
117, 10, 1wbr 4844 . . . . 5 wff 𝑧𝐴𝑦
128, 11wa 384 . . . 4 wff (𝑥𝐵𝑧𝑧𝐴𝑦)
1312, 6wex 1859 . . 3 wff 𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)
1413, 4, 9copab 4906 . 2 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
153, 14wceq 1637 1 wff (𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)}
Colors of variables: wff setvar class
This definition is referenced by:  coss1  5479  coss2  5480  nfco  5489  brcog  5490  cnvco  5509  cotrg  5717  relco  5847  coundi  5850  coundir  5851  cores  5852  xpco  5889  dffun2  6107  funco  6137  xpcomco  8285  coss12d  13932  xpcogend  13934  trclublem  13955  rtrclreclem3  14019  dfcoss3  34480
  Copyright terms: Public domain W3C validator