Definition df-co 4653

Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. Note that Definition 7 of [Suppes] p. 63 reverses 𝐴 and 𝐵, uses a slash 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 4648	. 2 class (𝐴 ∘ 𝐵)
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1363	. . . . . 6 class 𝑥
6		vz	. . . . . . 7 setvar 𝑧
7	6	cv 1363	. . . . . 6 class 𝑧
8	5, 7, 2	wbr 4018	. . . . 5 wff 𝑥𝐵𝑧
9		vy	. . . . . . 7 setvar 𝑦
10	9	cv 1363	. . . . . 6 class 𝑦
11	7, 10, 1	wbr 4018	. . . . 5 wff 𝑧𝐴𝑦
12	8, 11	wa 104	. . . 4 wff (𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)
13	12, 6	wex 1503	. . 3 wff ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)
14	13, 4, 9	copab 4078	. 2 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)}
15	3, 14	wceq 1364	1 wff (𝐴 ∘ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)}

This definition is referenced by:  coss1  4800  coss2  4801  nfco  4810  elco  4811  brcog  4812  cnvco  4830  cotr  5028  relco  5145  coundi  5148  coundir  5149  cores  5150  xpcom  5193  dffun2  5245  funco  5275  xpcomco  6853