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 28145) because (cos‘0) = 1 (see cos0 15493) and (exp‘1) = e (see df-e 15412). 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 5553 | . 2 class (𝐴 ∘ 𝐵) |
4 | vx | . . . . . . 7 setvar 𝑥 | |
5 | 4 | cv 1527 | . . . . . 6 class 𝑥 |
6 | vz | . . . . . . 7 setvar 𝑧 | |
7 | 6 | cv 1527 | . . . . . 6 class 𝑧 |
8 | 5, 7, 2 | wbr 5058 | . . . . 5 wff 𝑥𝐵𝑧 |
9 | vy | . . . . . . 7 setvar 𝑦 | |
10 | 9 | cv 1527 | . . . . . 6 class 𝑦 |
11 | 7, 10, 1 | wbr 5058 | . . . . 5 wff 𝑧𝐴𝑦 |
12 | 8, 11 | wa 396 | . . . 4 wff (𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) |
13 | 12, 6 | wex 1771 | . . 3 wff ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) |
14 | 13, 4, 9 | copab 5120 | . 2 class {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} |
15 | 3, 14 | wceq 1528 | 1 wff (𝐴 ∘ 𝐵) = {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} |
Colors of variables: wff setvar class |
This definition is referenced by: coss1 5720 coss2 5721 nfco 5730 brcog 5731 cnvco 5750 cotrg 5965 relco 6091 coundi 6094 coundir 6095 cores 6096 xpco 6134 dffun2 6359 funco 6389 xpcomco 8596 coss12d 14322 xpcogend 14324 trclublem 14345 rtrclreclem3 14409 dfcoss3 35544 |
Copyright terms: Public domain | W3C validator |