Definition df-co 5647

Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. For example, ((exp ∘ cos)‘0) = e (ex-co 30367) because (cos‘0) = 1 (see cos0 16118) and (exp‘1) = e (see df-e 16034). 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 5642	. 2 class (𝐴 ∘ 𝐵)
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1539	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1539	. . . . . 6 class 𝑧
8	5, 7, 2	wbr 5107	. . . . 5 wff 𝑥𝐵𝑧
9		vy	. . . . . . 7 setvar 𝑦
10	9	cv 1539	. . . . . 6 class 𝑦
11	7, 10, 1	wbr 5107	. . . . 5 wff 𝑧𝐴𝑦
12	8, 11	wa 395	. . . 4 wff (𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)
13	12, 6	wex 1779	. . 3 wff ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)
14	13, 4, 9	copab 5169	. 2 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)}
15	3, 14	wceq 1540	1 wff (𝐴 ∘ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)}

This definition is referenced by:  coss1  5819  coss2  5820  nfco  5829  brcog  5830  cnvco  5849  relco  6079  coundi  6220  coundir  6221  cores  6222  xpco  6262  dffun2OLDOLD  6523  funco  6556  xpcomco  9031  coss12d  14938  xpcogend  14940  trclublem  14961  rtrclreclem3  15026  bj-opabco  37176  bj-xpcossxp  37177  dfcoss3  38405