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 6092 | . 2 ⊢ Rel ((𝐴 ∘ 𝐵) ∘ 𝐶) | |
2 | relco 6092 | . 2 ⊢ Rel (𝐴 ∘ (𝐵 ∘ 𝐶)) | |
3 | excom 2164 | . . . 4 ⊢ (∃𝑧∃𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦)) ↔ ∃𝑤∃𝑧(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) | |
4 | anass 471 | . . . . 5 ⊢ (((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ (𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) | |
5 | 4 | 2exbii 1845 | . . . 4 ⊢ (∃𝑤∃𝑧((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ ∃𝑤∃𝑧(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) |
6 | 3, 5 | bitr4i 280 | . . 3 ⊢ (∃𝑧∃𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦)) ↔ ∃𝑤∃𝑧((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦)) |
7 | vex 3498 | . . . . . . 7 ⊢ 𝑧 ∈ V | |
8 | vex 3498 | . . . . . . 7 ⊢ 𝑦 ∈ V | |
9 | 7, 8 | brco 5736 | . . . . . 6 ⊢ (𝑧(𝐴 ∘ 𝐵)𝑦 ↔ ∃𝑤(𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦)) |
10 | 9 | anbi2i 624 | . . . . 5 ⊢ ((𝑥𝐶𝑧 ∧ 𝑧(𝐴 ∘ 𝐵)𝑦) ↔ (𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) |
11 | 10 | exbii 1844 | . . . 4 ⊢ (∃𝑧(𝑥𝐶𝑧 ∧ 𝑧(𝐴 ∘ 𝐵)𝑦) ↔ ∃𝑧(𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) |
12 | vex 3498 | . . . . 5 ⊢ 𝑥 ∈ V | |
13 | 12, 8 | opelco 5737 | . . . 4 ⊢ (〈𝑥, 𝑦〉 ∈ ((𝐴 ∘ 𝐵) ∘ 𝐶) ↔ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧(𝐴 ∘ 𝐵)𝑦)) |
14 | exdistr 1951 | . . . 4 ⊢ (∃𝑧∃𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦)) ↔ ∃𝑧(𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) | |
15 | 11, 13, 14 | 3bitr4i 305 | . . 3 ⊢ (〈𝑥, 𝑦〉 ∈ ((𝐴 ∘ 𝐵) ∘ 𝐶) ↔ ∃𝑧∃𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) |
16 | vex 3498 | . . . . . . 7 ⊢ 𝑤 ∈ V | |
17 | 12, 16 | brco 5736 | . . . . . 6 ⊢ (𝑥(𝐵 ∘ 𝐶)𝑤 ↔ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤)) |
18 | 17 | anbi1i 625 | . . . . 5 ⊢ ((𝑥(𝐵 ∘ 𝐶)𝑤 ∧ 𝑤𝐴𝑦) ↔ (∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦)) |
19 | 18 | exbii 1844 | . . . 4 ⊢ (∃𝑤(𝑥(𝐵 ∘ 𝐶)𝑤 ∧ 𝑤𝐴𝑦) ↔ ∃𝑤(∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦)) |
20 | 12, 8 | opelco 5737 | . . . 4 ⊢ (〈𝑥, 𝑦〉 ∈ (𝐴 ∘ (𝐵 ∘ 𝐶)) ↔ ∃𝑤(𝑥(𝐵 ∘ 𝐶)𝑤 ∧ 𝑤𝐴𝑦)) |
21 | 19.41v 1946 | . . . . 5 ⊢ (∃𝑧((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ (∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦)) | |
22 | 21 | exbii 1844 | . . . 4 ⊢ (∃𝑤∃𝑧((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ ∃𝑤(∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦)) |
23 | 19, 20, 22 | 3bitr4i 305 | . . 3 ⊢ (〈𝑥, 𝑦〉 ∈ (𝐴 ∘ (𝐵 ∘ 𝐶)) ↔ ∃𝑤∃𝑧((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦)) |
24 | 6, 15, 23 | 3bitr4i 305 | . 2 ⊢ (〈𝑥, 𝑦〉 ∈ ((𝐴 ∘ 𝐵) ∘ 𝐶) ↔ 〈𝑥, 𝑦〉 ∈ (𝐴 ∘ (𝐵 ∘ 𝐶))) |
25 | 1, 2, 24 | eqrelriiv 5658 | 1 ⊢ ((𝐴 ∘ 𝐵) ∘ 𝐶) = (𝐴 ∘ (𝐵 ∘ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 398 = wceq 1533 ∃wex 1776 ∈ wcel 2110 〈cop 4567 class class class wbr 5059 ∘ ccom 5554 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 ax-sep 5196 ax-nul 5203 ax-pr 5322 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3497 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-sn 4562 df-pr 4564 df-op 4568 df-br 5060 df-opab 5122 df-xp 5556 df-rel 5557 df-co 5559 |
This theorem is referenced by: funcoeqres 6640 fcof1oinvd 7043 tposco 7917 mapen 8675 mapfien 8865 hashfacen 13806 relexpsucnnl 14385 relexpaddnn 14404 cofuass 17153 setccatid 17338 estrccatid 17376 frmdup3lem 18025 symggrplem 18043 f1omvdco2 18570 symggen 18592 psgnunilem1 18615 gsumval3 19021 gsumzf1o 19026 gsumzmhm 19051 prds1 19358 psrass1lem 20151 pf1mpf 20509 pf1ind 20512 qtophmeo 22419 uniioombllem2 24178 cncombf 24253 motgrp 26323 pjsdi2i 29928 pjadj2coi 29975 pj3lem1 29977 pj3i 29979 fcoinver 30351 fmptco1f1o 30372 fcobij 30452 fcobijfs 30453 symgfcoeu 30721 pmtrcnel2 30729 cycpmconjv 30779 cycpmconjslem1 30791 cycpmconjs 30793 cyc3conja 30794 reprpmtf1o 31892 derangenlem 32413 subfacp1lem5 32426 erdsze2lem2 32446 pprodcnveq 33339 cocnv 34994 ltrncoidN 37258 trlcoabs2N 37852 trlcoat 37853 trlcone 37858 cdlemg46 37865 cdlemg47 37866 ltrnco4 37869 tgrpgrplem 37879 tendoplass 37913 cdlemi2 37949 cdlemk2 37962 cdlemk4 37964 cdlemk8 37968 cdlemk45 38077 cdlemk54 38088 cdlemk55a 38089 erngdvlem3 38120 erngdvlem3-rN 38128 tendocnv 38151 dvhvaddass 38227 dvhlveclem 38238 cdlemn8 38334 dihopelvalcpre 38378 dih1dimatlem0 38458 diophrw 39349 eldioph2 39352 mendring 39785 cortrcltrcl 40078 corclrtrcl 40079 cortrclrcl 40081 cotrclrtrcl 40082 cortrclrtrcl 40083 frege131d 40102 brcofffn 40374 brco3f1o 40376 neicvgnvo 40458 volicoff 42273 voliooicof 42274 ovolval4lem2 42925 isomushgr 43984 rngccatidALTV 44253 ringccatidALTV 44316 |
Copyright terms: Public domain | W3C validator |