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\circ B=\left\{⟨x,y⟩|\exists z\left(xBz\wedge zAy\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cB	$$classB$$
2	0 1	ccom	$$class\left(A\circ B\right)$$
3		vx	$$setvarx$$
4		vy	$$setvary$$
5		vz	$$setvarz$$
6	3	cv	$$setvarx$$
7	5	cv	$$setvarz$$
8	6 7 1	wbr	$$wffxBz$$
9	4	cv	$$setvary$$
10	7 9 0	wbr	$$wffzAy$$
11	8 10	wa	$$wff\left(xBz\wedge zAy\right)$$
12	11 5	wex	$$wff\exists z\left(xBz\wedge zAy\right)$$
13	12 3 4	copab	$$class\left\{⟨x,y⟩|\exists z\left(xBz\wedge zAy\right)\right\}$$
14	2 13	wceq	$$wffA\circ B=\left\{⟨x,y⟩|\exists z\left(xBz\wedge zAy\right)\right\}$$