Theorem coass 6281

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.) Remove dependency on ax-11 2197. (Revised by BJ, 25-Oct-2026.)

Assertion

Ref	Expression
coass	⊢ ((𝐴 ∘ 𝐵) ∘ 𝐶) = (𝐴 ∘ (𝐵 ∘ 𝐶))

Proof of Theorem coass

Dummy variables 𝑥 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		relco 6115	. 2 ⊢ Rel ((𝐴 ∘ 𝐵) ∘ 𝐶)
2		relco 6115	. 2 ⊢ Rel (𝐴 ∘ (𝐵 ∘ 𝐶))
3		vex 3458	. . . . 5 ⊢ 𝑥 ∈ V
4		vex 3458	. . . . 5 ⊢ 𝑦 ∈ V
5	3, 4	brco 5854	. . . 4 ⊢ (𝑥((𝐴 ∘ 𝐵) ∘ 𝐶)𝑦 ↔ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧(𝐴 ∘ 𝐵)𝑦))
6		vex 3458	. . . . . . . 8 ⊢ 𝑧 ∈ V
7	6, 4	brco 5854	. . . . . . 7 ⊢ (𝑧(𝐴 ∘ 𝐵)𝑦 ↔ ∃𝑤(𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))
8		vex 3458	. . . . . . . . . . . 12 ⊢ 𝑤 ∈ V
9	3, 6, 8	brcoi 5852	. . . . . . . . . . 11 ⊢ ((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) → 𝑥(𝐵 ∘ 𝐶)𝑤)
10	3, 8, 4	brcoi 5852	. . . . . . . . . . 11 ⊢ ((𝑥(𝐵 ∘ 𝐶)𝑤 ∧ 𝑤𝐴𝑦) → 𝑥(𝐴 ∘ (𝐵 ∘ 𝐶))𝑦)
11	9, 10	sylan 592	. . . . . . . . . 10 ⊢ (((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) → 𝑥(𝐴 ∘ (𝐵 ∘ 𝐶))𝑦)
12	11	anasss 472	. . . . . . . . 9 ⊢ ((𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦)) → 𝑥(𝐴 ∘ (𝐵 ∘ 𝐶))𝑦)
13	12	ex 418	. . . . . . . 8 ⊢ (𝑥𝐶𝑧 → ((𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦) → 𝑥(𝐴 ∘ (𝐵 ∘ 𝐶))𝑦))
14	13	exlimdv 1968	. . . . . . 7 ⊢ (𝑥𝐶𝑧 → (∃𝑤(𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦) → 𝑥(𝐴 ∘ (𝐵 ∘ 𝐶))𝑦))
15	7, 14	biimtrid 245	. . . . . 6 ⊢ (𝑥𝐶𝑧 → (𝑧(𝐴 ∘ 𝐵)𝑦 → 𝑥(𝐴 ∘ (𝐵 ∘ 𝐶))𝑦))
16	15	imp 412	. . . . 5 ⊢ ((𝑥𝐶𝑧 ∧ 𝑧(𝐴 ∘ 𝐵)𝑦) → 𝑥(𝐴 ∘ (𝐵 ∘ 𝐶))𝑦)
17	16	exlimiv 1965	. . . 4 ⊢ (∃𝑧(𝑥𝐶𝑧 ∧ 𝑧(𝐴 ∘ 𝐵)𝑦) → 𝑥(𝐴 ∘ (𝐵 ∘ 𝐶))𝑦)
18	5, 17	sylbi 220	. . 3 ⊢ (𝑥((𝐴 ∘ 𝐵) ∘ 𝐶)𝑦 → 𝑥(𝐴 ∘ (𝐵 ∘ 𝐶))𝑦)
19	3, 4	brco 5854	. . . 4 ⊢ (𝑥(𝐴 ∘ (𝐵 ∘ 𝐶))𝑦 ↔ ∃𝑤(𝑥(𝐵 ∘ 𝐶)𝑤 ∧ 𝑤𝐴𝑦))
20	3, 8	brco 5854	. . . . . . 7 ⊢ (𝑥(𝐵 ∘ 𝐶)𝑤 ↔ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤))
21	6, 8, 4	brcoi 5852	. . . . . . . . . . 11 ⊢ ((𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦) → 𝑧(𝐴 ∘ 𝐵)𝑦)
22	3, 6, 4	brcoi 5852	. . . . . . . . . . 11 ⊢ ((𝑥𝐶𝑧 ∧ 𝑧(𝐴 ∘ 𝐵)𝑦) → 𝑥((𝐴 ∘ 𝐵) ∘ 𝐶)𝑦)
23	21, 22	sylan2 605	. . . . . . . . . 10 ⊢ ((𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦)) → 𝑥((𝐴 ∘ 𝐵) ∘ 𝐶)𝑦)
24	23	anassrs 473	. . . . . . . . 9 ⊢ (((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) → 𝑥((𝐴 ∘ 𝐵) ∘ 𝐶)𝑦)
25	24	ex 418	. . . . . . . 8 ⊢ ((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) → (𝑤𝐴𝑦 → 𝑥((𝐴 ∘ 𝐵) ∘ 𝐶)𝑦))
26	25	exlimiv 1965	. . . . . . 7 ⊢ (∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) → (𝑤𝐴𝑦 → 𝑥((𝐴 ∘ 𝐵) ∘ 𝐶)𝑦))
27	20, 26	sylbi 220	. . . . . 6 ⊢ (𝑥(𝐵 ∘ 𝐶)𝑤 → (𝑤𝐴𝑦 → 𝑥((𝐴 ∘ 𝐵) ∘ 𝐶)𝑦))
28	27	imp 412	. . . . 5 ⊢ ((𝑥(𝐵 ∘ 𝐶)𝑤 ∧ 𝑤𝐴𝑦) → 𝑥((𝐴 ∘ 𝐵) ∘ 𝐶)𝑦)
29	28	exlimiv 1965	. . . 4 ⊢ (∃𝑤(𝑥(𝐵 ∘ 𝐶)𝑤 ∧ 𝑤𝐴𝑦) → 𝑥((𝐴 ∘ 𝐵) ∘ 𝐶)𝑦)
30	19, 29	sylbi 220	. . 3 ⊢ (𝑥(𝐴 ∘ (𝐵 ∘ 𝐶))𝑦 → 𝑥((𝐴 ∘ 𝐵) ∘ 𝐶)𝑦)
31	18, 30	impbii 212	. 2 ⊢ (𝑥((𝐴 ∘ 𝐵) ∘ 𝐶)𝑦 ↔ 𝑥(𝐴 ∘ (𝐵 ∘ 𝐶))𝑦)
32	1, 2, 31	eqbrriv 5772	1 ⊢ ((𝐴 ∘ 𝐵) ∘ 𝐶) = (𝐴 ∘ (𝐵 ∘ 𝐶))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  ∃wex 1812   class class class wbr 5106   ∘ ccom 5659

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-xp 5661  df-rel 5662  df-co 5664

This theorem is used by:  funcoeqres  6876  fcof1oinvd  7321  tposco  8299  mapen  9185  mapfien  9424  hashfacen  14623  relexpsucnnl  15209  relexpaddnn  15230  cofuass  18090  setccatid  18285  estrccatid  18332  frmdup3lem  19088  symggrplem  19106  f1omvdco2  19689  symggen  19711  psgnunilem1  19734  gsumval3  20148  gsumzf1o  20153  gsumzmhm  20178  prds1  20579  psrass1lem  22268  pf1mpf  22697  pf1ind  22700  qtophmeo  24163  uniioombllem2  25931  cncombf  26006  motgrp  29033  pjsdi2i  32786  pjadj2coi  32833  pj3lem1  32835  pj3i  32837  fcoinver  33267  fmptco1f1o  33296  fcobij  33379  fcobijfs  33380  cocnvf1o  33388  symgfcoeu  33710  pmtrcnel2  33718  cycpmconjv  33770  cycpmconjslem1  33782  cycpmconjs  33784  cyc3conja  33785  1arithidomlem2  34135  selvascl  34216  mplvrpmga  34244  mplvrpmrhm  34246  reprpmtf1o  35322  derangenlem  36102  subfacp1lem5  36115  erdsze2lem2  36135  pprodcnveq  36822  cocnv  38850  ltrncoidN  41376  trlcoabs2N  41970  trlcoat  41971  trlcone  41976  cdlemg46  41983  cdlemg47  41984  ltrnco4  41987  tgrpgrplem  41997  tendoplass  42031  cdlemi2  42067  cdlemk2  42080  cdlemk4  42082  cdlemk8  42086  cdlemk45  42195  cdlemk54  42206  cdlemk55a  42207  erngdvlem3  42238  erngdvlem3-rN  42246  tendocnv  42269  dvhvaddass  42345  dvhlveclem  42356  cdlemn8  42452  dihopelvalcpre  42496  dih1dimatlem0  42576  aks6d1c6lem5  43418  diophrw  43961  eldioph2  43964  mendring  44380  cortrcltrcl  44930  corclrtrcl  44931  cortrclrcl  44933  cotrclrtrcl  44934  cortrclrtrcl  44935  frege131d  44954  brcofffn  45221  brco3f1o  45223  neicvgnvo  45305  volicoff  47208  voliooicof  47209  ovolval4lem2  47863  3f1oss1  48348  gricushgr  49218  rngccatidALTV  49572  ringccatidALTV  49606  fuco11idx  50660