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

Definition df-co 4887
Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. For example,  ( ( exp 
o.  cos ) `  0
)  =  _e (ex-co 21746) because  ( cos `  0 )  =  1 (see cos0 12751) and  ( exp `  1
)  =  _e (see df-e 12671). 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 4882 . 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 4212 . . . . 5  wff  x B z
9 vy . . . . . . 7  set  y
109cv 1651 . . . . . 6  class  y
117, 10, 1wbr 4212 . . . . 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 4265 . 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  5028  coss2  5029  nfco  5038  brcog  5039  cnvco  5056  cotr  5246  relco  5368  coundi  5371  coundir  5372  cores  5373  xpco  5414  dffun2  5464  funco  5491  xpcomco  7198  rtrclreclem.trans  25146
  Copyright terms: Public domain W3C validator