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

Definition df-co 4846
Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. For example,  ( ( exp 
o.  cos ) `  0
)  =  _e (ex-co 21699) because  ( cos `  0 )  =  1 (see cos0 12706) and  ( exp `  1
)  =  _e (see df-e 12626). 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 4841 . 2  class  ( A  o.  B )
4 vx . . . . . . 7  set  x
54cv 1648 . . . . . 6  class  x
6 vz . . . . . . 7  set  z
76cv 1648 . . . . . 6  class  z
85, 7, 2wbr 4172 . . . . 5  wff  x B z
9 vy . . . . . . 7  set  y
109cv 1648 . . . . . 6  class  y
117, 10, 1wbr 4172 . . . . 5  wff  z A y
128, 11wa 359 . . . 4  wff  ( x B z  /\  z A y )
1312, 6wex 1547 . . 3  wff  E. z
( x B z  /\  z A y )
1413, 4, 9copab 4225 . 2  class  { <. x ,  y >.  |  E. z ( x B z  /\  z A y ) }
153, 14wceq 1649 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  4987  coss2  4988  nfco  4997  brcog  4998  cnvco  5015  cotr  5205  relco  5327  coundi  5330  coundir  5331  cores  5332  xpco  5373  dffun2  5423  funco  5450  xpcomco  7157  rtrclreclem.trans  25099
  Copyright terms: Public domain W3C validator