| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Associative law for class composition. Theorem 27 of [Suppes] p. 64. Also Exercise 21 of [Enderton] p. 53. Interestingly, this law holds for any classes whatsoever, not just functions or even relations. |
| Ref | Expression |
|---|---|
| coass |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | relco 3430 |
. 2
| |
| 2 | relco 3430 |
. 2
| |
| 3 | excom 1022 |
. . . 4
| |
| 4 | anass 439 |
. . . . 5
| |
| 5 | 4 | 2exbii 1028 |
. . . 4
|
| 6 | 3, 5 | bitr4 176 |
. . 3
|
| 7 | df-br 2588 |
. . . . . . 7
| |
| 8 | visset 1788 |
. . . . . . . 8
| |
| 9 | visset 1788 |
. . . . . . . 8
| |
| 10 | 8, 9 | opelco 3245 |
. . . . . . 7
|
| 11 | 7, 10 | bitr 173 |
. . . . . 6
|
| 12 | 11 | anbi2i 479 |
. . . . 5
|
| 13 | 12 | exbii 1027 |
. . . 4
|
| 14 | visset 1788 |
. . . . 5
| |
| 15 | 14, 9 | opelco 3245 |
. . . 4
|
| 16 | 19.42v 1290 |
. . . . 5
| |
| 17 | 16 | exbii 1027 |
. . . 4
|
| 18 | 13, 15, 17 | 3bitr4 183 |
. . 3
|
| 19 | df-br 2588 |
. . . . . . 7
| |
| 20 | visset 1788 |
. . . . . . . 8
| |
| 21 | 14, 20 | opelco 3245 |
. . . . . . 7
|
| 22 | 19, 21 | bitr 173 |
. . . . . 6
|
| 23 | 22 | anbi1i 480 |
. . . . 5
|
| 24 | 23 | exbii 1027 |
. . . 4
|
| 25 | 14, 9 | opelco 3245 |
. . . 4
|
| 26 | 19.41v 1287 |
. . . . 5
| |
| 27 | 26 | exbii 1027 |
. . . 4
|
| 28 | 24, 25, 27 | 3bitr4 183 |
. . 3
|
| 29 | 6, 18, 28 | 3bitr4 183 |
. 2
|
| 30 | 1, 2, 29 | eqrelriv 3213 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: mapenlem1 4421 mapenlem2 4422 symggrpi 8673 hmeogrp 8776 pjsdi2 10210 pjadj2co 10256 pj3lem1 10258 pj3 10260 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-4 951 ax-5 952 ax-6 953 ax-7 954 ax-gen 955 ax-8 1101 ax-9 1102 ax-10 1103 ax-12 1104 ax-13 1107 ax-14 1108 ax-11 1180 ax-17 1190 ax-16 1194 ax-11o 1202 ax-ext 1436 ax-sep 2671 ax-pow 2710 ax-pr 2747 |
| This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-ex 957 df-sb 1155 df-eu 1359 df-mo 1360 df-clab 1441 df-cleq 1446 df-clel 1449 df-ne 1563 df-v 1787 df-dif 2020 df-un 2021 df-in 2022 df-ss 2024 df-nul 2252 df-pw 2373 df-sn 2383 df-pr 2384 df-op 2387 df-br 2588 df-opab 2635 df-xp 3147 df-rel 3148 df-co 3150 |