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

Definition df-co 4698
Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. For example,  ( ( exp 
o.  cos ) `  0
)  =  _e (ex-co 20825) because  ( cos `  0 )  =  1 (see cos0 12430) and  ( exp `  1
)  =  _e (see df-e 12350). 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 4693 . 2  class  ( A  o.  B )
4 vx . . . . . . 7  set  x
54cv 1622 . . . . . 6  class  x
6 vz . . . . . . 7  set  z
76cv 1622 . . . . . 6  class  z
85, 7, 2wbr 4023 . . . . 5  wff  x B z
9 vy . . . . . . 7  set  y
109cv 1622 . . . . . 6  class  y
117, 10, 1wbr 4023 . . . . 5  wff  z A y
128, 11wa 358 . . . 4  wff  ( x B z  /\  z A y )
1312, 6wex 1528 . . 3  wff  E. z
( x B z  /\  z A y )
1413, 4, 9copab 4076 . 2  class  { <. x ,  y >.  |  E. z ( x B z  /\  z A y ) }
153, 14wceq 1623 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  4839  coss2  4840  nfco  4849  brcog  4850  cnvco  4865  cotr  5055  relco  5171  coundi  5174  coundir  5175  cores  5176  dffun2  5265  funco  5292  xpcomco  6952  rtrclreclem.trans  24043  inposet  25278
  Copyright terms: Public domain W3C validator