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

Definition df-co 4643
Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. For example,  ( ( exp 
o.  cos ) `  0
)  =  _e (ex-co 20733) because  ( cos `  0 )  =  1 (see cos0 12357) and  ( exp `  1
)  =  _e (see df-e 12277). 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 4630 . 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 3963 . . . . 5  wff  x B z
9 vy . . . . . . 7  set  y
109cv 1618 . . . . . 6  class  y
117, 10, 1wbr 3963 . . . . 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 4016 . 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  4792  coss2  4793  nfco  4802  brcog  4803  cnvco  4818  cotr  5008  relco  5123  coundi  5126  coundir  5127  cores  5128  dffun2  5169  funco  5195  xpcomco  6885  rtrclreclem.trans  23380  inposet  24610
  Copyright terms: Public domain W3C validator