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 6087 | . 2 ⊢ Rel ((𝐴 ∘ 𝐵) ∘ 𝐶) | |
2 | relco 6087 | . 2 ⊢ Rel (𝐴 ∘ (𝐵 ∘ 𝐶)) | |
3 | excom 2170 | . . . 4 ⊢ (∃𝑧∃𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦)) ↔ ∃𝑤∃𝑧(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) | |
4 | anass 472 | . . . . 5 ⊢ (((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ (𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) | |
5 | 4 | 2exbii 1855 | . . . 4 ⊢ (∃𝑤∃𝑧((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ ∃𝑤∃𝑧(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) |
6 | 3, 5 | bitr4i 281 | . . 3 ⊢ (∃𝑧∃𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦)) ↔ ∃𝑤∃𝑧((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦)) |
7 | vex 3404 | . . . . . . 7 ⊢ 𝑧 ∈ V | |
8 | vex 3404 | . . . . . . 7 ⊢ 𝑦 ∈ V | |
9 | 7, 8 | brco 5723 | . . . . . 6 ⊢ (𝑧(𝐴 ∘ 𝐵)𝑦 ↔ ∃𝑤(𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦)) |
10 | 9 | anbi2i 626 | . . . . 5 ⊢ ((𝑥𝐶𝑧 ∧ 𝑧(𝐴 ∘ 𝐵)𝑦) ↔ (𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) |
11 | 10 | exbii 1854 | . . . 4 ⊢ (∃𝑧(𝑥𝐶𝑧 ∧ 𝑧(𝐴 ∘ 𝐵)𝑦) ↔ ∃𝑧(𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) |
12 | vex 3404 | . . . . 5 ⊢ 𝑥 ∈ V | |
13 | 12, 8 | opelco 5724 | . . . 4 ⊢ (〈𝑥, 𝑦〉 ∈ ((𝐴 ∘ 𝐵) ∘ 𝐶) ↔ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧(𝐴 ∘ 𝐵)𝑦)) |
14 | exdistr 1962 | . . . 4 ⊢ (∃𝑧∃𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦)) ↔ ∃𝑧(𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) | |
15 | 11, 13, 14 | 3bitr4i 306 | . . 3 ⊢ (〈𝑥, 𝑦〉 ∈ ((𝐴 ∘ 𝐵) ∘ 𝐶) ↔ ∃𝑧∃𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))) |
16 | vex 3404 | . . . . . . 7 ⊢ 𝑤 ∈ V | |
17 | 12, 16 | brco 5723 | . . . . . 6 ⊢ (𝑥(𝐵 ∘ 𝐶)𝑤 ↔ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤)) |
18 | 17 | anbi1i 627 | . . . . 5 ⊢ ((𝑥(𝐵 ∘ 𝐶)𝑤 ∧ 𝑤𝐴𝑦) ↔ (∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦)) |
19 | 18 | exbii 1854 | . . . 4 ⊢ (∃𝑤(𝑥(𝐵 ∘ 𝐶)𝑤 ∧ 𝑤𝐴𝑦) ↔ ∃𝑤(∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦)) |
20 | 12, 8 | opelco 5724 | . . . 4 ⊢ (〈𝑥, 𝑦〉 ∈ (𝐴 ∘ (𝐵 ∘ 𝐶)) ↔ ∃𝑤(𝑥(𝐵 ∘ 𝐶)𝑤 ∧ 𝑤𝐴𝑦)) |
21 | 19.41v 1957 | . . . . 5 ⊢ (∃𝑧((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ (∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦)) | |
22 | 21 | exbii 1854 | . . . 4 ⊢ (∃𝑤∃𝑧((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ ∃𝑤(∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦)) |
23 | 19, 20, 22 | 3bitr4i 306 | . . 3 ⊢ (〈𝑥, 𝑦〉 ∈ (𝐴 ∘ (𝐵 ∘ 𝐶)) ↔ ∃𝑤∃𝑧((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦)) |
24 | 6, 15, 23 | 3bitr4i 306 | . 2 ⊢ (〈𝑥, 𝑦〉 ∈ ((𝐴 ∘ 𝐵) ∘ 𝐶) ↔ 〈𝑥, 𝑦〉 ∈ (𝐴 ∘ (𝐵 ∘ 𝐶))) |
25 | 1, 2, 24 | eqrelriiv 5644 | 1 ⊢ ((𝐴 ∘ 𝐵) ∘ 𝐶) = (𝐴 ∘ (𝐵 ∘ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 399 = wceq 1542 ∃wex 1786 ∈ wcel 2114 〈cop 4532 class class class wbr 5040 ∘ ccom 5539 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-11 2162 ax-12 2179 ax-ext 2711 ax-sep 5177 ax-nul 5184 ax-pr 5306 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-sb 2075 df-clab 2718 df-cleq 2731 df-clel 2812 df-v 3402 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-nul 4222 df-if 4425 df-sn 4527 df-pr 4529 df-op 4533 df-br 5041 df-opab 5103 df-xp 5541 df-rel 5542 df-co 5544 |
This theorem is referenced by: funcoeqres 6660 fcof1oinvd 7072 tposco 7964 mapen 8743 mapfien 8957 hashfacen 13916 hashfacenOLD 13917 relexpsucnnl 14491 relexpaddnn 14512 cofuass 17276 setccatid 17468 estrccatid 17510 frmdup3lem 18159 symggrplem 18177 f1omvdco2 18706 symggen 18728 psgnunilem1 18751 gsumval3 19158 gsumzf1o 19163 gsumzmhm 19188 prds1 19498 psrass1lemOLD 20765 psrass1lem 20768 pf1mpf 21134 pf1ind 21137 qtophmeo 22580 uniioombllem2 24347 cncombf 24422 motgrp 26501 pjsdi2i 30104 pjadj2coi 30151 pj3lem1 30153 pj3i 30155 fcoinver 30532 fmptco1f1o 30554 fcobij 30644 fcobijfs 30645 symgfcoeu 30940 pmtrcnel2 30948 cycpmconjv 30998 cycpmconjslem1 31010 cycpmconjs 31012 cyc3conja 31013 reprpmtf1o 32188 derangenlem 32716 subfacp1lem5 32729 erdsze2lem2 32749 pprodcnveq 33840 cocnv 35538 ltrncoidN 37797 trlcoabs2N 38391 trlcoat 38392 trlcone 38397 cdlemg46 38404 cdlemg47 38405 ltrnco4 38408 tgrpgrplem 38418 tendoplass 38452 cdlemi2 38488 cdlemk2 38501 cdlemk4 38503 cdlemk8 38507 cdlemk45 38616 cdlemk54 38627 cdlemk55a 38628 erngdvlem3 38659 erngdvlem3-rN 38667 tendocnv 38690 dvhvaddass 38766 dvhlveclem 38777 cdlemn8 38873 dihopelvalcpre 38917 dih1dimatlem0 38997 diophrw 40193 eldioph2 40196 mendring 40629 cortrcltrcl 40934 corclrtrcl 40935 cortrclrcl 40937 cotrclrtrcl 40938 cortrclrtrcl 40939 frege131d 40958 brcofffn 41227 brco3f1o 41229 neicvgnvo 41311 volicoff 43118 voliooicof 43119 ovolval4lem2 43770 isomushgr 44859 rngccatidALTV 45128 ringccatidALTV 45191 |
Copyright terms: Public domain | W3C validator |