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

Definition df-co 4597
Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. For example,  ( ( exp 
o.  cos ) `  0
)  =  _e (ex-co 20638) because  ( cos `  0 )  =  1 (see cos0 12304) and  ( exp `  1
)  =  _e (see df-e 12224). 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 4584 . 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 3920 . . . . 5  wff  x B z
9 vy . . . . . . 7  set  y
109cv 1618 . . . . . 6  class  y
117, 10, 1wbr 3920 . . . . 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 3973 . 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  4746  coss2  4747  nfco  4756  brcog  4757  cnvco  4772  cotr  4962  relco  5077  coundi  5080  coundir  5081  cores  5082  dffun2  5123  funco  5149  xpcomco  6837  rtrclreclem.trans  23214  inposet  24444
  Copyright terms: Public domain W3C validator