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

Definition df-co 4422
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 4417 . 2  class  ( A  o.  B )
4 vx . . . . . . 7  setvar  x
54cv 1286 . . . . . 6  class  x
6 vz . . . . . . 7  setvar  z
76cv 1286 . . . . . 6  class  z
85, 7, 2wbr 3822 . . . . 5  wff  x B z
9 vy . . . . . . 7  setvar  y
109cv 1286 . . . . . 6  class  y
117, 10, 1wbr 3822 . . . . 5  wff  z A y
128, 11wa 102 . . . 4  wff  ( x B z  /\  z A y )
1312, 6wex 1424 . . 3  wff  E. z
( x B z  /\  z A y )
1413, 4, 9copab 3875 . 2  class  { <. x ,  y >.  |  E. z ( x B z  /\  z A y ) }
153, 14wceq 1287 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  4561  coss2  4562  nfco  4571  elco  4572  brcog  4573  cnvco  4591  cotr  4782  relco  4897  coundi  4900  coundir  4901  cores  4902  xpcom  4945  dffun2  4993  funco  5021  xpcomco  6496
  Copyright terms: Public domain W3C validator