Definition df-co 5589

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

This definition is referenced by:  coss1  5753  coss2  5754  nfco  5763  brcog  5764  cnvco  5783  cotrg  6005  relco  6137  coundi  6140  coundir  6141  cores  6142  xpco  6181  dffun2  6428  funco  6458  xpcomco  8802  coss12d  14611  xpcogend  14613  trclublem  14634  rtrclreclem3  14699  bj-opabco  35286  bj-xpcossxp  35287  dfcoss3  36467