Theorem coass 6085

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.)

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 6064	. 2 ⊢ Rel ((𝐴 ∘ 𝐵) ∘ 𝐶)
2		relco 6064	. 2 ⊢ Rel (𝐴 ∘ (𝐵 ∘ 𝐶))
3		excom 2166	. . . 4 ⊢ (∃𝑧∃𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦)) ↔ ∃𝑤∃𝑧(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦)))
4		anass 472	. . . . 5 ⊢ (((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ (𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦)))
5	4	2exbii 1850	. . . 4 ⊢ (∃𝑤∃𝑧((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ ∃𝑤∃𝑧(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦)))
6	3, 5	bitr4i 281	. . 3 ⊢ (∃𝑧∃𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦)) ↔ ∃𝑤∃𝑧((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
7		vex 3444	. . . . . . 7 ⊢ 𝑧 ∈ V
8		vex 3444	. . . . . . 7 ⊢ 𝑦 ∈ V
9	7, 8	brco 5705	. . . . . 6 ⊢ (𝑧(𝐴 ∘ 𝐵)𝑦 ↔ ∃𝑤(𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦))
10	9	anbi2i 625	. . . . 5 ⊢ ((𝑥𝐶𝑧 ∧ 𝑧(𝐴 ∘ 𝐵)𝑦) ↔ (𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦)))
11	10	exbii 1849	. . . 4 ⊢ (∃𝑧(𝑥𝐶𝑧 ∧ 𝑧(𝐴 ∘ 𝐵)𝑦) ↔ ∃𝑧(𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦)))
12		vex 3444	. . . . 5 ⊢ 𝑥 ∈ V
13	12, 8	opelco 5706	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ ((𝐴 ∘ 𝐵) ∘ 𝐶) ↔ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧(𝐴 ∘ 𝐵)𝑦))
14		exdistr 1955	. . . 4 ⊢ (∃𝑧∃𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦)) ↔ ∃𝑧(𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦)))
15	11, 13, 14	3bitr4i 306	. . 3 ⊢ (⟨𝑥, 𝑦⟩ ∈ ((𝐴 ∘ 𝐵) ∘ 𝐶) ↔ ∃𝑧∃𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤 ∧ 𝑤𝐴𝑦)))
16		vex 3444	. . . . . . 7 ⊢ 𝑤 ∈ V
17	12, 16	brco 5705	. . . . . 6 ⊢ (𝑥(𝐵 ∘ 𝐶)𝑤 ↔ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤))
18	17	anbi1i 626	. . . . 5 ⊢ ((𝑥(𝐵 ∘ 𝐶)𝑤 ∧ 𝑤𝐴𝑦) ↔ (∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
19	18	exbii 1849	. . . 4 ⊢ (∃𝑤(𝑥(𝐵 ∘ 𝐶)𝑤 ∧ 𝑤𝐴𝑦) ↔ ∃𝑤(∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
20	12, 8	opelco 5706	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ (𝐵 ∘ 𝐶)) ↔ ∃𝑤(𝑥(𝐵 ∘ 𝐶)𝑤 ∧ 𝑤𝐴𝑦))
21		19.41v 1950	. . . . 5 ⊢ (∃𝑧((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ (∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
22	21	exbii 1849	. . . 4 ⊢ (∃𝑤∃𝑧((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ ∃𝑤(∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
23	19, 20, 22	3bitr4i 306	. . 3 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ (𝐵 ∘ 𝐶)) ↔ ∃𝑤∃𝑧((𝑥𝐶𝑧 ∧ 𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
24	6, 15, 23	3bitr4i 306	. 2 ⊢ (⟨𝑥, 𝑦⟩ ∈ ((𝐴 ∘ 𝐵) ∘ 𝐶) ↔ ⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ (𝐵 ∘ 𝐶)))
25	1, 2, 24	eqrelriiv 5627	1 ⊢ ((𝐴 ∘ 𝐵) ∘ 𝐶) = (𝐴 ∘ (𝐵 ∘ 𝐶))

Syntax hints:   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ⟨cop 4531   class class class wbr 5030   ∘ ccom 5523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-xp 5525  df-rel 5526  df-co 5528

This theorem is referenced by:  funcoeqres  6620  fcof1oinvd  7027  tposco  7906  mapen  8665  mapfien  8855  hashfacen  13808  relexpsucnnl  14381  relexpaddnn  14402  cofuass  17151  setccatid  17336  estrccatid  17374  frmdup3lem  18023  symggrplem  18041  f1omvdco2  18568  symggen  18590  psgnunilem1  18613  gsumval3  19020  gsumzf1o  19025  gsumzmhm  19050  prds1  19360  psrass1lem  20615  pf1mpf  20976  pf1ind  20979  qtophmeo  22422  uniioombllem2  24187  cncombf  24262  motgrp  26337  pjsdi2i  29940  pjadj2coi  29987  pj3lem1  29989  pj3i  29991  fcoinver  30370  fmptco1f1o  30392  fcobij  30484  fcobijfs  30485  symgfcoeu  30776  pmtrcnel2  30784  cycpmconjv  30834  cycpmconjslem1  30846  cycpmconjs  30848  cyc3conja  30849  reprpmtf1o  32007  derangenlem  32531  subfacp1lem5  32544  erdsze2lem2  32564  pprodcnveq  33457  cocnv  35163  ltrncoidN  37424  trlcoabs2N  38018  trlcoat  38019  trlcone  38024  cdlemg46  38031  cdlemg47  38032  ltrnco4  38035  tgrpgrplem  38045  tendoplass  38079  cdlemi2  38115  cdlemk2  38128  cdlemk4  38130  cdlemk8  38134  cdlemk45  38243  cdlemk54  38254  cdlemk55a  38255  erngdvlem3  38286  erngdvlem3-rN  38294  tendocnv  38317  dvhvaddass  38393  dvhlveclem  38404  cdlemn8  38500  dihopelvalcpre  38544  dih1dimatlem0  38624  diophrw  39700  eldioph2  39703  mendring  40136  cortrcltrcl  40441  corclrtrcl  40442  cortrclrcl  40444  cotrclrtrcl  40445  cortrclrtrcl  40446  frege131d  40465  brcofffn  40734  brco3f1o  40736  neicvgnvo  40818  volicoff  42637  voliooicof  42638  ovolval4lem2  43289  isomushgr  44344  rngccatidALTV  44613  ringccatidALTV  44676