This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) }