Definition df-co 5123

Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. For example, ( ( exp o. cos ) ` 0 ) = _e (ex-co 27295) because ( cos ` 0 ) = 1 (see cos0 14880) and ( exp ` 1 ) = _e (see df-e 14799). 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

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	ccom 5118	. 2 class ( A o. B )
4		vx	. . . . . . 7 setvar x
5	4	cv 1482	. . . . . 6 class x
6		vz	. . . . . . 7 setvar z
7	6	cv 1482	. . . . . 6 class z
8	5, 7, 2	wbr 4653	. . . . 5 wff x B z
9		vy	. . . . . . 7 setvar y
10	9	cv 1482	. . . . . 6 class y
11	7, 10, 1	wbr 4653	. . . . 5 wff z A y
12	8, 11	wa 384	. . . 4 wff ( x B z /\ z A y )
13	12, 6	wex 1704	. . 3 wff E. z ( x B z /\ z A y )
14	13, 4, 9	copab 4712	. 2 class { <. x , y >. | E. z ( x B z /\ z A y ) }
15	3, 14	wceq 1483	1 wff ( A o. B ) = { <. x , y >. | E. z ( x B z /\ z A y ) }

This definition is referenced by:  coss1  5277  coss2  5278  nfco  5287  brcog  5288  cnvco  5308  cotrg  5507  relco  5633  coundi  5636  coundir  5637  cores  5638  xpco  5675  dffun2  5898  funco  5928  xpcomco  8050  coss12d  13711  xpcogend  13713  trclublem  13734  rtrclreclem3  13800