ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-co Unicode version

Definition df-co 4516
Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. Note that Definition 7 of [Suppes] p. 63 reverses  A and  B, uses a slash 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 4511 . 2  class  ( A  o.  B )
4 vx . . . . . . 7  setvar  x
54cv 1313 . . . . . 6  class  x
6 vz . . . . . . 7  setvar  z
76cv 1313 . . . . . 6  class  z
85, 7, 2wbr 3897 . . . . 5  wff  x B z
9 vy . . . . . . 7  setvar  y
109cv 1313 . . . . . 6  class  y
117, 10, 1wbr 3897 . . . . 5  wff  z A y
128, 11wa 103 . . . 4  wff  ( x B z  /\  z A y )
1312, 6wex 1451 . . 3  wff  E. z
( x B z  /\  z A y )
1413, 4, 9copab 3956 . 2  class  { <. x ,  y >.  |  E. z ( x B z  /\  z A y ) }
153, 14wceq 1314 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  4662  coss2  4663  nfco  4672  elco  4673  brcog  4674  cnvco  4692  cotr  4888  relco  5005  coundi  5008  coundir  5009  cores  5010  xpcom  5053  dffun2  5101  funco  5131  xpcomco  6686
  Copyright terms: Public domain W3C validator