![]() |
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 6108 | . 2 ⊢ Rel ((𝐴 ∘ 𝐵) ∘ 𝐶) | |
2 | relco 6108 | . 2 ⊢ Rel (𝐴 ∘ (𝐵 ∘ 𝐶)) | |
3 | excom 2163 | . . . 4 ⊢ (∃𝑧∃𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦)) ↔ ∃𝑤∃𝑧(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) | |
4 | anass 470 | . . . . 5 ⊢ (((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ (𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) | |
5 | 4 | 2exbii 1852 | . . . 4 ⊢ (∃𝑤∃𝑧((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ ∃𝑤∃𝑧(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) |
6 | 3, 5 | bitr4i 278 | . . 3 ⊢ (∃𝑧∃𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦)) ↔ ∃𝑤∃𝑧((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦)) |
7 | vex 3479 | . . . . . . 7 ⊢ 𝑧 ∈ V | |
8 | vex 3479 | . . . . . . 7 ⊢ 𝑦 ∈ V | |
9 | 7, 8 | brco 5871 | . . . . . 6 ⊢ (𝑧(𝐴 ∘ 𝐵)𝑦 ↔ ∃𝑤(𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦)) |
10 | 9 | anbi2i 624 | . . . . 5 ⊢ ((𝑥𝐶𝑧 ∧ 𝑧(𝐴 ∘ 𝐵)𝑦) ↔ (𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) |
11 | 10 | exbii 1851 | . . . 4 ⊢ (∃𝑧(𝑥𝐶𝑧 ∧ 𝑧(𝐴 ∘ 𝐵)𝑦) ↔ ∃𝑧(𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) |
12 | vex 3479 | . . . . 5 ⊢ 𝑥 ∈ V | |
13 | 12, 8 | opelco 5872 | . . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ ((𝐴 ∘ 𝐵) ∘ 𝐶) ↔ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧(𝐴 ∘ 𝐵)𝑦)) |
14 | exdistr 1959 | . . . 4 ⊢ (∃𝑧∃𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦)) ↔ ∃𝑧(𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) | |
15 | 11, 13, 14 | 3bitr4i 303 | . . 3 ⊢ (⟨𝑥, 𝑦⟩ ∈ ((𝐴 ∘ 𝐵) ∘ 𝐶) ↔ ∃𝑧∃𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) |
16 | vex 3479 | . . . . . . 7 ⊢ 𝑤 ∈ V | |
17 | 12, 16 | brco 5871 | . . . . . 6 ⊢ (𝑥(𝐵 ∘ 𝐶)𝑤 ↔ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤)) |
18 | 17 | anbi1i 625 | . . . . 5 ⊢ ((𝑥(𝐵 ∘ 𝐶)𝑤 ∧ 𝑤𝐴𝑦) ↔ (∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦)) |
19 | 18 | exbii 1851 | . . . 4 ⊢ (∃𝑤(𝑥(𝐵 ∘ 𝐶)𝑤 ∧ 𝑤𝐴𝑦) ↔ ∃𝑤(∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦)) |
20 | 12, 8 | opelco 5872 | . . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ (𝐵 ∘ 𝐶)) ↔ ∃𝑤(𝑥(𝐵 ∘ 𝐶)𝑤 ∧ 𝑤𝐴𝑦)) |
21 | 19.41v 1954 | . . . . 5 ⊢ (∃𝑧((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ (∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦)) | |
22 | 21 | exbii 1851 | . . . 4 ⊢ (∃𝑤∃𝑧((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ ∃𝑤(∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦)) |
23 | 19, 20, 22 | 3bitr4i 303 | . . 3 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ (𝐵 ∘ 𝐶)) ↔ ∃𝑤∃𝑧((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦)) |
24 | 6, 15, 23 | 3bitr4i 303 | . 2 ⊢ (⟨𝑥, 𝑦⟩ ∈ ((𝐴 ∘ 𝐵) ∘ 𝐶) ↔ ⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ (𝐵 ∘ 𝐶))) |
25 | 1, 2, 24 | eqrelriiv 5791 | 1 ⊢ ((𝐴 ∘ 𝐵) ∘ 𝐶) = (𝐴 ∘ (𝐵 ∘ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 397 = wceq 1542 ∃wex 1782 ∈ wcel 2107 ⟨cop 4635 class class class wbr 5149 ∘ ccom 5681 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-11 2155 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pr 5428 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-br 5150 df-opab 5212 df-xp 5683 df-rel 5684 df-co 5686 |
This theorem is referenced by: funcoeqres 6865 fcof1oinvd 7291 tposco 8242 mapen 9141 mapfien 9403 hashfacen 14413 hashfacenOLD 14414 relexpsucnnl 14977 relexpaddnn 14998 cofuass 17839 setccatid 18034 estrccatid 18083 frmdup3lem 18747 symggrplem 18765 f1omvdco2 19316 symggen 19338 psgnunilem1 19361 gsumval3 19775 gsumzf1o 19780 gsumzmhm 19805 prds1 20136 psrass1lemOLD 21493 psrass1lem 21496 pf1mpf 21871 pf1ind 21874 qtophmeo 23321 uniioombllem2 25100 cncombf 25175 motgrp 27794 pjsdi2i 31410 pjadj2coi 31457 pj3lem1 31459 pj3i 31461 fcoinver 31835 fmptco1f1o 31857 fcobij 31947 fcobijfs 31948 symgfcoeu 32243 pmtrcnel2 32251 cycpmconjv 32301 cycpmconjslem1 32313 cycpmconjs 32315 cyc3conja 32316 reprpmtf1o 33638 derangenlem 34162 subfacp1lem5 34175 erdsze2lem2 34195 pprodcnveq 34855 cocnv 36593 ltrncoidN 38999 trlcoabs2N 39593 trlcoat 39594 trlcone 39599 cdlemg46 39606 cdlemg47 39607 ltrnco4 39610 tgrpgrplem 39620 tendoplass 39654 cdlemi2 39690 cdlemk2 39703 cdlemk4 39705 cdlemk8 39709 cdlemk45 39818 cdlemk54 39829 cdlemk55a 39830 erngdvlem3 39861 erngdvlem3-rN 39869 tendocnv 39892 dvhvaddass 39968 dvhlveclem 39979 cdlemn8 40075 dihopelvalcpre 40119 dih1dimatlem0 40199 diophrw 41497 eldioph2 41500 mendring 41934 cortrcltrcl 42491 corclrtrcl 42492 cortrclrcl 42494 cotrclrtrcl 42495 cortrclrtrcl 42496 frege131d 42515 brcofffn 42782 brco3f1o 42784 neicvgnvo 42866 volicoff 44711 voliooicof 44712 ovolval4lem2 45366 isomushgr 46494 rngccatidALTV 46887 ringccatidALTV 46950 |
Copyright terms: Public domain | W3C validator |