![]() |
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 30371) because (cos‘0) = 1 (see cos0 16152) and (exp‘1) = e (see df-e 16070). 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 5686 | . 2 class (𝐴 ∘ 𝐵) |
4 | vx | . . . . . . 7 setvar 𝑥 | |
5 | 4 | cv 1533 | . . . . . 6 class 𝑥 |
6 | vz | . . . . . . 7 setvar 𝑧 | |
7 | 6 | cv 1533 | . . . . . 6 class 𝑧 |
8 | 5, 7, 2 | wbr 5153 | . . . . 5 wff 𝑥𝐵𝑧 |
9 | vy | . . . . . . 7 setvar 𝑦 | |
10 | 9 | cv 1533 | . . . . . 6 class 𝑦 |
11 | 7, 10, 1 | wbr 5153 | . . . . 5 wff 𝑧𝐴𝑦 |
12 | 8, 11 | wa 394 | . . . 4 wff (𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) |
13 | 12, 6 | wex 1774 | . . 3 wff ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) |
14 | 13, 4, 9 | copab 5215 | . 2 class {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} |
15 | 3, 14 | wceq 1534 | 1 wff (𝐴 ∘ 𝐵) = {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} |
Colors of variables: wff setvar class |
This definition is referenced by: coss1 5862 coss2 5863 nfco 5872 brcog 5873 cnvco 5892 relco 6118 coundi 6258 coundir 6259 cores 6260 xpco 6300 dffun2OLDOLD 6566 funco 6599 xpcomco 9100 coss12d 14977 xpcogend 14979 trclublem 15000 rtrclreclem3 15065 bj-opabco 36895 bj-xpcossxp 36896 dfcoss3 38112 |
Copyright terms: Public domain | W3C validator |