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 27295) because (cos‘0) = 1 (see cos0 14880) and (exp‘1) = e (see df-e 14799). 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 5118 | . 2 class (𝐴 ∘ 𝐵) |
4 | vx | . . . . . . 7 setvar 𝑥 | |
5 | 4 | cv 1482 | . . . . . 6 class 𝑥 |
6 | vz | . . . . . . 7 setvar 𝑧 | |
7 | 6 | cv 1482 | . . . . . 6 class 𝑧 |
8 | 5, 7, 2 | wbr 4653 | . . . . 5 wff 𝑥𝐵𝑧 |
9 | vy | . . . . . . 7 setvar 𝑦 | |
10 | 9 | cv 1482 | . . . . . 6 class 𝑦 |
11 | 7, 10, 1 | wbr 4653 | . . . . 5 wff 𝑧𝐴𝑦 |
12 | 8, 11 | wa 384 | . . . 4 wff (𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) |
13 | 12, 6 | wex 1704 | . . 3 wff ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) |
14 | 13, 4, 9 | copab 4712 | . 2 class {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} |
15 | 3, 14 | wceq 1483 | 1 wff (𝐴 ∘ 𝐵) = {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} |
Colors of variables: wff setvar class |
This definition is referenced by: coss1 5277 coss2 5278 nfco 5287 brcog 5288 cnvco 5308 cotrg 5507 relco 5633 coundi 5636 coundir 5637 cores 5638 xpco 5675 dffun2 5898 funco 5928 xpcomco 8050 coss12d 13711 xpcogend 13713 trclublem 13734 rtrclreclem3 13800 |
Copyright terms: Public domain | W3C validator |