Definition df-co 4003

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 3990	. 2 class (A o. B)
4		vx	. . . . . . 7 set x
5	4	cv 1297	. . . . . 6 class x
6		vz	. . . . . . 7 set z
7	6	cv 1297	. . . . . 6 class z
8	5, 7, 2	wbr 3338	. . . . 5 wff xBz
9		vy	. . . . . . 7 set y
10	9	cv 1297	. . . . . 6 class y
11	7, 10, 1	wbr 3338	. . . . 5 wff zAy
12	8, 11	wa 240	. . . 4 wff (xBz /\ zAy)
13	12, 6	wex 1326	. . 3 wff E.z(xBz /\ zAy)
14	13, 4, 9	copab 3395	. 2 class {<.x, y>. | E.z(xBz /\ zAy)}
15	3, 14	wceq 1298	1 wff (A o. B) = {<.x, y>. | E.z(xBz /\ zAy)}

This definition is referenced by:  coeq1 4123  coeq2 4124  hbco 4129  opelco 4130  opelcoOLD 4131  cnvco 4145  cnvcoOLD 4146  cotr 4302  cotrOLD 4303  relco 4392  coundi 4396  coundir 4398  cores 4400  dffun2 4431  funco 4457  inclrel 14444  inposet 14620

Copyright terms: Public domain