| 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 30457) because (cos‘0) = 1 (see cos0 16186) and (exp‘1) = e (see df-e 16104). 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 5689 | . 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 5143 | . . . . 5 wff 𝑥𝐵𝑧 |
| 9 | vy | . . . . . . 7 setvar 𝑦 | |
| 10 | 9 | cv 1539 | . . . . . 6 class 𝑦 |
| 11 | 7, 10, 1 | wbr 5143 | . . . . 5 wff 𝑧𝐴𝑦 |
| 12 | 8, 11 | wa 395 | . . . 4 wff (𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) |
| 13 | 12, 6 | wex 1779 | . . 3 wff ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) |
| 14 | 13, 4, 9 | copab 5205 | . 2 class {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} |
| 15 | 3, 14 | wceq 1540 | 1 wff (𝐴 ∘ 𝐵) = {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} |
| Colors of variables: wff setvar class |
| This definition is referenced by: coss1 5866 coss2 5867 nfco 5876 brcog 5877 cnvco 5896 relco 6126 coundi 6267 coundir 6268 cores 6269 xpco 6309 dffun2OLDOLD 6573 funco 6606 xpcomco 9102 coss12d 15011 xpcogend 15013 trclublem 15034 rtrclreclem3 15099 bj-opabco 37189 bj-xpcossxp 37190 dfcoss3 38415 |
| Copyright terms: Public domain | W3C validator |