| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > coass | Structured version Visualization version GIF 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. (Contributed by NM, 27-Jan-1997.) |
| Ref | Expression |
|---|---|
| coass | ⊢ ((𝐴 ∘ 𝐵) ∘ 𝐶) = (𝐴 ∘ (𝐵 ∘ 𝐶)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | relco 6126 | . 2 ⊢ Rel ((𝐴 ∘ 𝐵) ∘ 𝐶) | |
| 2 | relco 6126 | . 2 ⊢ Rel (𝐴 ∘ (𝐵 ∘ 𝐶)) | |
| 3 | excom 2162 | . . . 4 ⊢ (∃𝑧∃𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦)) ↔ ∃𝑤∃𝑧(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) | |
| 4 | anass 468 | . . . . 5 ⊢ (((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ (𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) | |
| 5 | 4 | 2exbii 1849 | . . . 4 ⊢ (∃𝑤∃𝑧((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ ∃𝑤∃𝑧(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) |
| 6 | 3, 5 | bitr4i 278 | . . 3 ⊢ (∃𝑧∃𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦)) ↔ ∃𝑤∃𝑧((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦)) |
| 7 | vex 3484 | . . . . . . 7 ⊢ 𝑧 ∈ V | |
| 8 | vex 3484 | . . . . . . 7 ⊢ 𝑦 ∈ V | |
| 9 | 7, 8 | brco 5881 | . . . . . 6 ⊢ (𝑧(𝐴 ∘ 𝐵)𝑦 ↔ ∃𝑤(𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦)) |
| 10 | 9 | anbi2i 623 | . . . . 5 ⊢ ((𝑥𝐶𝑧 ∧ 𝑧(𝐴 ∘ 𝐵)𝑦) ↔ (𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) |
| 11 | 10 | exbii 1848 | . . . 4 ⊢ (∃𝑧(𝑥𝐶𝑧 ∧ 𝑧(𝐴 ∘ 𝐵)𝑦) ↔ ∃𝑧(𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) |
| 12 | vex 3484 | . . . . 5 ⊢ 𝑥 ∈ V | |
| 13 | 12, 8 | opelco 5882 | . . . 4 ⊢ (〈𝑥, 𝑦〉 ∈ ((𝐴 ∘ 𝐵) ∘ 𝐶) ↔ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧(𝐴 ∘ 𝐵)𝑦)) |
| 14 | exdistr 1954 | . . . 4 ⊢ (∃𝑧∃𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦)) ↔ ∃𝑧(𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) | |
| 15 | 11, 13, 14 | 3bitr4i 303 | . . 3 ⊢ (〈𝑥, 𝑦〉 ∈ ((𝐴 ∘ 𝐵) ∘ 𝐶) ↔ ∃𝑧∃𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) |
| 16 | vex 3484 | . . . . . . 7 ⊢ 𝑤 ∈ V | |
| 17 | 12, 16 | brco 5881 | . . . . . 6 ⊢ (𝑥(𝐵 ∘ 𝐶)𝑤 ↔ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤)) |
| 18 | 17 | anbi1i 624 | . . . . 5 ⊢ ((𝑥(𝐵 ∘ 𝐶)𝑤 ∧ 𝑤𝐴𝑦) ↔ (∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦)) |
| 19 | 18 | exbii 1848 | . . . 4 ⊢ (∃𝑤(𝑥(𝐵 ∘ 𝐶)𝑤 ∧ 𝑤𝐴𝑦) ↔ ∃𝑤(∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦)) |
| 20 | 12, 8 | opelco 5882 | . . . 4 ⊢ (〈𝑥, 𝑦〉 ∈ (𝐴 ∘ (𝐵 ∘ 𝐶)) ↔ ∃𝑤(𝑥(𝐵 ∘ 𝐶)𝑤 ∧ 𝑤𝐴𝑦)) |
| 21 | 19.41v 1949 | . . . . 5 ⊢ (∃𝑧((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ (∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦)) | |
| 22 | 21 | exbii 1848 | . . . 4 ⊢ (∃𝑤∃𝑧((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ ∃𝑤(∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦)) |
| 23 | 19, 20, 22 | 3bitr4i 303 | . . 3 ⊢ (〈𝑥, 𝑦〉 ∈ (𝐴 ∘ (𝐵 ∘ 𝐶)) ↔ ∃𝑤∃𝑧((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦)) |
| 24 | 6, 15, 23 | 3bitr4i 303 | . 2 ⊢ (〈𝑥, 𝑦〉 ∈ ((𝐴 ∘ 𝐵) ∘ 𝐶) ↔ 〈𝑥, 𝑦〉 ∈ (𝐴 ∘ (𝐵 ∘ 𝐶))) |
| 25 | 1, 2, 24 | eqrelriiv 5800 | 1 ⊢ ((𝐴 ∘ 𝐵) ∘ 𝐶) = (𝐴 ∘ (𝐵 ∘ 𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: ∧ wa 395 = wceq 1540 ∃wex 1779 ∈ wcel 2108 〈cop 4632 class class class wbr 5143 ∘ ccom 5689 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-11 2157 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-br 5144 df-opab 5206 df-xp 5691 df-rel 5692 df-co 5694 |
| This theorem is referenced by: funcoeqres 6879 fcof1oinvd 7313 tposco 8282 mapen 9181 mapfien 9448 hashfacen 14493 relexpsucnnl 15069 relexpaddnn 15090 cofuass 17934 setccatid 18129 estrccatid 18176 frmdup3lem 18879 symggrplem 18897 f1omvdco2 19466 symggen 19488 psgnunilem1 19511 gsumval3 19925 gsumzf1o 19930 gsumzmhm 19955 prds1 20320 psrass1lem 21952 pf1mpf 22356 pf1ind 22359 qtophmeo 23825 uniioombllem2 25618 cncombf 25693 motgrp 28551 pjsdi2i 32176 pjadj2coi 32223 pj3lem1 32225 pj3i 32227 fcoinver 32617 fmptco1f1o 32643 fcobij 32733 fcobijfs 32734 symgfcoeu 33102 pmtrcnel2 33110 cycpmconjv 33162 cycpmconjslem1 33174 cycpmconjs 33176 cyc3conja 33177 1arithidomlem2 33564 reprpmtf1o 34641 derangenlem 35176 subfacp1lem5 35189 erdsze2lem2 35209 pprodcnveq 35884 cocnv 37732 ltrncoidN 40130 trlcoabs2N 40724 trlcoat 40725 trlcone 40730 cdlemg46 40737 cdlemg47 40738 ltrnco4 40741 tgrpgrplem 40751 tendoplass 40785 cdlemi2 40821 cdlemk2 40834 cdlemk4 40836 cdlemk8 40840 cdlemk45 40949 cdlemk54 40960 cdlemk55a 40961 erngdvlem3 40992 erngdvlem3-rN 41000 tendocnv 41023 dvhvaddass 41099 dvhlveclem 41110 cdlemn8 41206 dihopelvalcpre 41250 dih1dimatlem0 41330 aks6d1c6lem5 42178 diophrw 42770 eldioph2 42773 mendring 43200 cortrcltrcl 43753 corclrtrcl 43754 cortrclrcl 43756 cotrclrtrcl 43757 cortrclrtrcl 43758 frege131d 43777 brcofffn 44044 brco3f1o 44046 neicvgnvo 44128 volicoff 46010 voliooicof 46011 ovolval4lem2 46665 3f1oss1 47087 gricushgr 47886 rngccatidALTV 48188 ringccatidALTV 48222 fuco11idx 49030 |
| Copyright terms: Public domain | W3C validator |