![]() |
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 6128 | . 2 ⊢ Rel ((𝐴 ∘ 𝐵) ∘ 𝐶) | |
2 | relco 6128 | . 2 ⊢ Rel (𝐴 ∘ (𝐵 ∘ 𝐶)) | |
3 | excom 2159 | . . . 4 ⊢ (∃𝑧∃𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦)) ↔ ∃𝑤∃𝑧(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) | |
4 | anass 468 | . . . . 5 ⊢ (((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ (𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) | |
5 | 4 | 2exbii 1845 | . . . 4 ⊢ (∃𝑤∃𝑧((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ ∃𝑤∃𝑧(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) |
6 | 3, 5 | bitr4i 278 | . . 3 ⊢ (∃𝑧∃𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦)) ↔ ∃𝑤∃𝑧((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦)) |
7 | vex 3481 | . . . . . . 7 ⊢ 𝑧 ∈ V | |
8 | vex 3481 | . . . . . . 7 ⊢ 𝑦 ∈ V | |
9 | 7, 8 | brco 5883 | . . . . . 6 ⊢ (𝑧(𝐴 ∘ 𝐵)𝑦 ↔ ∃𝑤(𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦)) |
10 | 9 | anbi2i 623 | . . . . 5 ⊢ ((𝑥𝐶𝑧 ∧ 𝑧(𝐴 ∘ 𝐵)𝑦) ↔ (𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) |
11 | 10 | exbii 1844 | . . . 4 ⊢ (∃𝑧(𝑥𝐶𝑧 ∧ 𝑧(𝐴 ∘ 𝐵)𝑦) ↔ ∃𝑧(𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) |
12 | vex 3481 | . . . . 5 ⊢ 𝑥 ∈ V | |
13 | 12, 8 | opelco 5884 | . . . 4 ⊢ (〈𝑥, 𝑦〉 ∈ ((𝐴 ∘ 𝐵) ∘ 𝐶) ↔ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧(𝐴 ∘ 𝐵)𝑦)) |
14 | exdistr 1951 | . . . 4 ⊢ (∃𝑧∃𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦)) ↔ ∃𝑧(𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) | |
15 | 11, 13, 14 | 3bitr4i 303 | . . 3 ⊢ (〈𝑥, 𝑦〉 ∈ ((𝐴 ∘ 𝐵) ∘ 𝐶) ↔ ∃𝑧∃𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) |
16 | vex 3481 | . . . . . . 7 ⊢ 𝑤 ∈ V | |
17 | 12, 16 | brco 5883 | . . . . . 6 ⊢ (𝑥(𝐵 ∘ 𝐶)𝑤 ↔ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤)) |
18 | 17 | anbi1i 624 | . . . . 5 ⊢ ((𝑥(𝐵 ∘ 𝐶)𝑤 ∧ 𝑤𝐴𝑦) ↔ (∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦)) |
19 | 18 | exbii 1844 | . . . 4 ⊢ (∃𝑤(𝑥(𝐵 ∘ 𝐶)𝑤 ∧ 𝑤𝐴𝑦) ↔ ∃𝑤(∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦)) |
20 | 12, 8 | opelco 5884 | . . . 4 ⊢ (〈𝑥, 𝑦〉 ∈ (𝐴 ∘ (𝐵 ∘ 𝐶)) ↔ ∃𝑤(𝑥(𝐵 ∘ 𝐶)𝑤 ∧ 𝑤𝐴𝑦)) |
21 | 19.41v 1946 | . . . . 5 ⊢ (∃𝑧((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ (∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦)) | |
22 | 21 | exbii 1844 | . . . 4 ⊢ (∃𝑤∃𝑧((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ ∃𝑤(∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦)) |
23 | 19, 20, 22 | 3bitr4i 303 | . . 3 ⊢ (〈𝑥, 𝑦〉 ∈ (𝐴 ∘ (𝐵 ∘ 𝐶)) ↔ ∃𝑤∃𝑧((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦)) |
24 | 6, 15, 23 | 3bitr4i 303 | . 2 ⊢ (〈𝑥, 𝑦〉 ∈ ((𝐴 ∘ 𝐵) ∘ 𝐶) ↔ 〈𝑥, 𝑦〉 ∈ (𝐴 ∘ (𝐵 ∘ 𝐶))) |
25 | 1, 2, 24 | eqrelriiv 5802 | 1 ⊢ ((𝐴 ∘ 𝐵) ∘ 𝐶) = (𝐴 ∘ (𝐵 ∘ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 395 = wceq 1536 ∃wex 1775 ∈ wcel 2105 〈cop 4636 class class class wbr 5147 ∘ ccom 5692 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-11 2154 ax-ext 2705 ax-sep 5301 ax-nul 5311 ax-pr 5437 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-rab 3433 df-v 3479 df-dif 3965 df-un 3967 df-ss 3979 df-nul 4339 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-br 5148 df-opab 5210 df-xp 5694 df-rel 5695 df-co 5697 |
This theorem is referenced by: funcoeqres 6879 fcof1oinvd 7312 tposco 8280 mapen 9179 mapfien 9445 hashfacen 14489 relexpsucnnl 15065 relexpaddnn 15086 cofuass 17939 setccatid 18137 estrccatid 18186 frmdup3lem 18891 symggrplem 18909 f1omvdco2 19480 symggen 19502 psgnunilem1 19525 gsumval3 19939 gsumzf1o 19944 gsumzmhm 19969 prds1 20336 psrass1lem 21969 pf1mpf 22371 pf1ind 22374 qtophmeo 23840 uniioombllem2 25631 cncombf 25706 motgrp 28565 pjsdi2i 32185 pjadj2coi 32232 pj3lem1 32234 pj3i 32236 fcoinver 32623 fmptco1f1o 32649 fcobij 32739 fcobijfs 32740 symgfcoeu 33084 pmtrcnel2 33092 cycpmconjv 33144 cycpmconjslem1 33156 cycpmconjs 33158 cyc3conja 33159 1arithidomlem2 33543 reprpmtf1o 34619 derangenlem 35155 subfacp1lem5 35168 erdsze2lem2 35188 pprodcnveq 35864 cocnv 37711 ltrncoidN 40110 trlcoabs2N 40704 trlcoat 40705 trlcone 40710 cdlemg46 40717 cdlemg47 40718 ltrnco4 40721 tgrpgrplem 40731 tendoplass 40765 cdlemi2 40801 cdlemk2 40814 cdlemk4 40816 cdlemk8 40820 cdlemk45 40929 cdlemk54 40940 cdlemk55a 40941 erngdvlem3 40972 erngdvlem3-rN 40980 tendocnv 41003 dvhvaddass 41079 dvhlveclem 41090 cdlemn8 41186 dihopelvalcpre 41230 dih1dimatlem0 41310 aks6d1c6lem5 42158 diophrw 42746 eldioph2 42749 mendring 43176 cortrcltrcl 43729 corclrtrcl 43730 cortrclrcl 43732 cotrclrtrcl 43733 cortrclrtrcl 43734 frege131d 43753 brcofffn 44020 brco3f1o 44022 neicvgnvo 44104 volicoff 45950 voliooicof 45951 ovolval4lem2 46605 3f1oss1 47024 gricushgr 47823 rngccatidALTV 48115 ringccatidALTV 48149 |
Copyright terms: Public domain | W3C validator |