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

Definition df-co 4664
Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. For example,  ( ( exp 
o.  cos ) `  0
)  =  _e (ex-co 20754) because  ( cos `  0 )  =  1 (see cos0 12378) and  ( exp `  1
)  =  _e (see df-e 12298). 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 4651 . 2  class  ( A  o.  B )
4 vx . . . . . . 7  set  x
54cv 1618 . . . . . 6  class  x
6 vz . . . . . . 7  set  z
76cv 1618 . . . . . 6  class  z
85, 7, 2wbr 3983 . . . . 5  wff  x B z
9 vy . . . . . . 7  set  y
109cv 1618 . . . . . 6  class  y
117, 10, 1wbr 3983 . . . . 5  wff  z A y
128, 11wa 360 . . . 4  wff  ( x B z  /\  z A y )
1312, 6wex 1537 . . 3  wff  E. z
( x B z  /\  z A y )
1413, 4, 9copab 4036 . 2  class  { <. x ,  y >.  |  E. z ( x B z  /\  z A y ) }
153, 14wceq 1619 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  4813  coss2  4814  nfco  4823  brcog  4824  cnvco  4839  cotr  5029  relco  5144  coundi  5147  coundir  5148  cores  5149  dffun2  5190  funco  5216  xpcomco  6906  rtrclreclem.trans  23401  inposet  24631
  Copyright terms: Public domain W3C validator