Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-co | Structured version Visualization version GIF version |
Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. For example, ((exp ∘ cos)‘0) = e (ex-co 28217) because (cos‘0) = 1 (see cos0 15503) and (exp‘1) = e (see df-e 15422). 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.) |
Ref | Expression |
---|---|
df-co | ⊢ (𝐴 ∘ 𝐵) = {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | 1, 2 | ccom 5559 | . 2 class (𝐴 ∘ 𝐵) |
4 | vx | . . . . . . 7 setvar 𝑥 | |
5 | 4 | cv 1536 | . . . . . 6 class 𝑥 |
6 | vz | . . . . . . 7 setvar 𝑧 | |
7 | 6 | cv 1536 | . . . . . 6 class 𝑧 |
8 | 5, 7, 2 | wbr 5066 | . . . . 5 wff 𝑥𝐵𝑧 |
9 | vy | . . . . . . 7 setvar 𝑦 | |
10 | 9 | cv 1536 | . . . . . 6 class 𝑦 |
11 | 7, 10, 1 | wbr 5066 | . . . . 5 wff 𝑧𝐴𝑦 |
12 | 8, 11 | wa 398 | . . . 4 wff (𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) |
13 | 12, 6 | wex 1780 | . . 3 wff ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) |
14 | 13, 4, 9 | copab 5128 | . 2 class {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} |
15 | 3, 14 | wceq 1537 | 1 wff (𝐴 ∘ 𝐵) = {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} |
Colors of variables: wff setvar class |
This definition is referenced by: coss1 5726 coss2 5727 nfco 5736 brcog 5737 cnvco 5756 cotrg 5971 relco 6097 coundi 6100 coundir 6101 cores 6102 xpco 6140 dffun2 6365 funco 6395 xpcomco 8607 coss12d 14332 xpcogend 14334 trclublem 14355 rtrclreclem3 14419 dfcoss3 35677 |
Copyright terms: Public domain | W3C validator |