MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-co Structured version   Unicode version

Definition df-co 4879
Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. For example,  ( ( exp 
o.  cos ) `  0
)  =  _e (ex-co 21738) because  ( cos `  0 )  =  1 (see cos0 12743) and  ( exp `  1
)  =  _e (see df-e 12663). Note that Definition 7 of [Suppes] p. 63 reverses  A and  B, uses  /. instead of  o., and calls the operation "relative product." (Contributed by NM, 4-Jul-1994.)
Assertion
Ref Expression
df-co  |-  ( A  o.  B )  =  { <. x ,  y
>.  |  E. z
( x B z  /\  z A y ) }
Distinct variable groups:    x, y,
z, A    x, B, y, z

Detailed syntax breakdown of Definition df-co
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
31, 2ccom 4874 . 2  class  ( A  o.  B )
4 vx . . . . . . 7  set  x
54cv 1651 . . . . . 6  class  x
6 vz . . . . . . 7  set  z
76cv 1651 . . . . . 6  class  z
85, 7, 2wbr 4204 . . . . 5  wff  x B z
9 vy . . . . . . 7  set  y
109cv 1651 . . . . . 6  class  y
117, 10, 1wbr 4204 . . . . 5  wff  z A y
128, 11wa 359 . . . 4  wff  ( x B z  /\  z A y )
1312, 6wex 1550 . . 3  wff  E. z
( x B z  /\  z A y )
1413, 4, 9copab 4257 . 2  class  { <. x ,  y >.  |  E. z ( x B z  /\  z A y ) }
153, 14wceq 1652 1  wff  ( A  o.  B )  =  { <. x ,  y
>.  |  E. z
( x B z  /\  z A y ) }
Colors of variables: wff set class
This definition is referenced by:  coss1  5020  coss2  5021  nfco  5030  brcog  5031  cnvco  5048  cotr  5238  relco  5360  coundi  5363  coundir  5364  cores  5365  xpco  5406  dffun2  5456  funco  5483  xpcomco  7190  rtrclreclem.trans  25138
  Copyright terms: Public domain W3C validator