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

Definition df-co 4297
Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. Note that Definition 7 of [Suppes] p. 63 reverses and , uses a slash instead of  o., and calls the operation "relative product." (Contributed by NM, 4-Jul-1994.)
Assertion
Ref Expression
df-co  o.  { <. , 
>.  |  }
Distinct variable groups:   ,,,   ,,,

Detailed syntax breakdown of Definition df-co
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2ccom 4292 . 2  o.
4 vx . . . . . . 7  setvar
54cv 1241 . . . . . 6
6 vz . . . . . . 7  setvar
76cv 1241 . . . . . 6
85, 7, 2wbr 3755 . . . . 5
9 vy . . . . . . 7  setvar
109cv 1241 . . . . . 6
117, 10, 1wbr 3755 . . . . 5
128, 11wa 97 . . . 4
1312, 6wex 1378 . . 3
1413, 4, 9copab 3808 . 2  { <. ,  >.  |  }
153, 14wceq 1242 1  o.  { <. , 
>.  |  }
Colors of variables: wff set class
This definition is referenced by:  coss1  4434  coss2  4435  nfco  4444  brcog  4445  cnvco  4463  cotr  4649  relco  4762  coundi  4765  coundir  4766  cores  4767  xpcom  4807  dffun2  4855  funco  4883  xpcomco  6236
  Copyright terms: Public domain W3C validator