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 20801) because  ( cos `  0 )  =  1 (see cos0 12425) and  ( exp `  1
)  =  _e (see df-e 12345). 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 1623 . . . . . 6  class  x
6 vz . . . . . . 7  set  z
76cv 1623 . . . . . 6  class  z
85, 7, 2wbr 4025 . . . . 5  wff  x B z
9 vy . . . . . . 7  set  y
109cv 1623 . . . . . 6  class  y
117, 10, 1wbr 4025 . . . . 5  wff  z A y
128, 11wa 360 . . . 4  wff  ( x B z  /\  z A y )
1312, 6wex 1529 . . 3  wff  E. z
( x B z  /\  z A y )
1413, 4, 9copab 4078 . 2  class  { <. x ,  y >.  |  E. z ( x B z  /\  z A y ) }
153, 14wceq 1624 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  5170  coundi  5173  coundir  5174  cores  5175  dffun2  5232  funco  5258  xpcomco  6948  rtrclreclem.trans  23448  inposet  24678
  Copyright terms: Public domain W3C validator