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

Definition df-co 4714
Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. For example,  ( ( exp 
o.  cos ) `  0
)  =  _e (ex-co 20841) because  ( cos `  0 )  =  1 (see cos0 12446) and  ( exp `  1
)  =  _e (see df-e 12366). 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 4709 . 2  class  ( A  o.  B )
4 vx . . . . . . 7  set  x
54cv 1631 . . . . . 6  class  x
6 vz . . . . . . 7  set  z
76cv 1631 . . . . . 6  class  z
85, 7, 2wbr 4039 . . . . 5  wff  x B z
9 vy . . . . . . 7  set  y
109cv 1631 . . . . . 6  class  y
117, 10, 1wbr 4039 . . . . 5  wff  z A y
128, 11wa 358 . . . 4  wff  ( x B z  /\  z A y )
1312, 6wex 1531 . . 3  wff  E. z
( x B z  /\  z A y )
1413, 4, 9copab 4092 . 2  class  { <. x ,  y >.  |  E. z ( x B z  /\  z A y ) }
153, 14wceq 1632 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  4855  coss2  4856  nfco  4865  brcog  4866  cnvco  4881  cotr  5071  relco  5187  coundi  5190  coundir  5191  cores  5192  dffun2  5281  funco  5308  xpcomco  6968  rtrclreclem.trans  24058  inposet  25381
  Copyright terms: Public domain W3C validator