Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-co | GIF version |
Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. Note that Definition 7 of [Suppes] p. 63 reverses 𝐴 and 𝐵, uses a slash 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 4543 | . 2 class (𝐴 ∘ 𝐵) |
4 | vx | . . . . . . 7 setvar 𝑥 | |
5 | 4 | cv 1330 | . . . . . 6 class 𝑥 |
6 | vz | . . . . . . 7 setvar 𝑧 | |
7 | 6 | cv 1330 | . . . . . 6 class 𝑧 |
8 | 5, 7, 2 | wbr 3929 | . . . . 5 wff 𝑥𝐵𝑧 |
9 | vy | . . . . . . 7 setvar 𝑦 | |
10 | 9 | cv 1330 | . . . . . 6 class 𝑦 |
11 | 7, 10, 1 | wbr 3929 | . . . . 5 wff 𝑧𝐴𝑦 |
12 | 8, 11 | wa 103 | . . . 4 wff (𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) |
13 | 12, 6 | wex 1468 | . . 3 wff ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) |
14 | 13, 4, 9 | copab 3988 | . 2 class {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} |
15 | 3, 14 | wceq 1331 | 1 wff (𝐴 ∘ 𝐵) = {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} |
Colors of variables: wff set class |
This definition is referenced by: coss1 4694 coss2 4695 nfco 4704 elco 4705 brcog 4706 cnvco 4724 cotr 4920 relco 5037 coundi 5040 coundir 5041 cores 5042 xpcom 5085 dffun2 5133 funco 5163 xpcomco 6720 |
Copyright terms: Public domain | W3C validator |