Definition df-co 5416

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

This definition is referenced by:  coss1  5576  coss2  5577  nfco  5586  brcog  5587  cnvco  5606  cotrg  5811  relco  5936  coundi  5939  coundir  5940  cores  5941  xpco  5978  dffun2  6198  funco  6228  xpcomco  8403  coss12d  14193  xpcogend  14195  trclublem  14216  rtrclreclem3  14280  dfcoss3  35113