Definition df-co 4168

Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. Note that Definition 7 of [Suppes] p. 63 reverses A and B, uses /. instead of o., and calls the operation "relative product."

Assertion

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

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 4155	. 2 class (A o. B)
4		vx	. . . . . . 7 set x
5	4	cv 1614	. . . . . 6 class x
6		vz	. . . . . . 7 set z
7	6	cv 1614	. . . . . 6 class z
8	5, 7, 2	wbr 3539	. . . . 5 wff xBz
9		vy	. . . . . . 7 set y
10	9	cv 1614	. . . . . 6 class y
11	7, 10, 1	wbr 3539	. . . . 5 wff zAy
12	8, 11	wa 433	. . . 4 wff (xBz /\ zAy)
13	12, 6	wex 1644	. . 3 wff E.z(xBz /\ zAy)
14	13, 4, 9	copab 3597	. 2 class {<.x, y>. | E.z(xBz /\ zAy)}
15	3, 14	wceq 1615	1 wff (A o. B) = {<.x, y>. | E.z(xBz /\ zAy)}

This definition is referenced by:  coss1 4280  coss2 4281  hbco 4290  opelco 4291  cnvco 4304  cotr 4452  relco 4532  coundi 4535  coundir 4536  cores 4537  dffun2 4573  funco 4598  inclrelOLD 15417  inposet 15620

Copyright terms: Public domain