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

Definition df-co 4928
Description: Define the composition of two classes. Definition 6.6(3) of ?Error: exp o. cos ) ` 0 ) = _e ^^^ This math symbol is not active (i.e. was not declared in this scope). [TakeutiZaring] p. 24. For example, (( o. )`0)= ?Error: cos ` 0 ) = 1 ^^^ This math symbol is not active (i.e. was not declared in this scope). (ex-co 21797) because ( `0)=1 (see cos0 12802) and ?Error: exp ` 1 ) = _e ^^^ This math symbol is not active (i.e. was not declared in this scope). ( `1)= (see df-e 12722). Note that Definition 7 of [Suppes] ?Error: /. ^^ This math symbol is not active (i.e. was not declared in this scope). p. 63 reverses and , uses /. instead of o., and calls the operation "relative product." (Contributed by NM, 4-Jul-1994.)
Assertion
Ref Expression
df-co
Distinct variable groups:   , , ,   , , ,

Detailed syntax breakdown of Definition df-co
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2ccom 4923 . 2
4 vx . . . . . . 7
54cv 1653 . . . . . 6
6 vz . . . . . . 7
76cv 1653 . . . . . 6
85, 7, 2wbr 4243 . . . . 5
9 vy . . . . . . 7
109cv 1653 . . . . . 6
117, 10, 1wbr 4243 . . . . 5
128, 11wa 360 . . . 4
1312, 6wex 1551 . . 3
1413, 4, 9copab 4300 . 2
153, 14wceq 1654 1
Colors of variables: wff set class
This definition is referenced by:  coss1  5070  coss2  5071  nfco  5080  brcog  5081  cnvco  5100  cotr  5290  relco  5414  coundi  5417  coundir  5418  cores  5419  xpco  5460  dffun2  5511  funco  5538  xpcomco  7247  rtrclreclem.trans  25250
  Copyright terms: Public domain W3C validator