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

Definition df-co 4878
Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. For example,  ( ( exp 
o.  cos ) `  0
)  =  _e (ex-co 21734) because  ( cos `  0 )  =  1 (see cos0 12739) and  ( exp `  1
)  =  _e (see df-e 12659). 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 4873 . 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  5019  coss2  5020  nfco  5029  brcog  5030  cnvco  5047  cotr  5237  relco  5359  coundi  5362  coundir  5363  cores  5364  xpco  5405  dffun2  5455  funco  5482  xpcomco  7189  rtrclreclem.trans  25134
  Copyright terms: Public domain W3C validator