Definition df-co

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

	Ref	Expression
Assertion	df-co	|- ( A o. B ) = { <. x , y >. | E. z ( x B z /\ z A y ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1		cB	|- B
2	0 1	ccom	|- ( A o. B )
3		vx	|- x
4		vy	|- y
5		vz	|- z
6	3	cv	|- x
7	5	cv	|- z
8	6 7 1	wbr	|- x B z
9	4	cv	|- y
10	7 9 0	wbr	|- z A y
11	8 10	wa	|- ( x B z /\ z A y )
12	11 5	wex	|- E. z ( x B z /\ z A y )
13	12 3 4	copab	|- { <. x , y >. | E. z ( x B z /\ z A y ) }
14	2 13	wceq	|- ( A o. B ) = { <. x , y >. | E. z ( x B z /\ z A y ) }