Definition df-co 5645

Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. For example, ((exp ∘ cos)‘0) = e (ex-co 30575) because (cos‘0) = 1 (see cos0 16154) and (exp‘1) = e (see df-e 16070). Note that Definition 7 of [Suppes] p. 63 reverses 𝐴 and 𝐵, uses / instead of ∘, and calls the operation "relative product". (Contributed by NM, 4-Jul-1994.)

Assertion

Ref	Expression
df-co	⊢ (𝐴 ∘ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)}

Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑥,𝐵,𝑦,𝑧

Detailed syntax breakdown of Definition df-co

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	ccom 5640	. 2 class (𝐴 ∘ 𝐵)
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1549	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1549	. . . . . 6 class 𝑧
8	5, 7, 2	wbr 5090	. . . . 5 wff 𝑥𝐵𝑧
9		vy	. . . . . . 7 setvar 𝑦
10	9	cv 1549	. . . . . 6 class 𝑦
11	7, 10, 1	wbr 5090	. . . . 5 wff 𝑧𝐴𝑦
12	8, 11	wa 398	. . . 4 wff (𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)
13	12, 6	wex 1789	. . 3 wff ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)
14	13, 4, 9	copab 5152	. 2 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)}
15	3, 14	wceq 1550	1 wff (𝐴 ∘ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)}

This definition is referenced by:  coss1  5816  coss2  5817  nfco  5826  brcog  5827  cnvco  5850  relco  6083  coundi  6219  coundir  6220  cores  6221  xpco  6261  funco  6546  xpcomco  9024  coss12d  14971  xpcogend  14973  trclublem  14994  rtrclreclem3  15059  dfsuccf2  36229  bj-opabco  37618  bj-xpcossxp  37619  dfcoss3  38941