MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  coass Structured version   Visualization version   GIF version

Theorem coass 6264
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.
StepHypRef Expression
1 relco 6107 . 2 Rel ((𝐴𝐵) ∘ 𝐶)
2 relco 6107 . 2 Rel (𝐴 ∘ (𝐵𝐶))
3 excom 2161 . . . 4 (∃𝑧𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)) ↔ ∃𝑤𝑧(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)))
4 anass 468 . . . . 5 (((𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ (𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)))
542exbii 1850 . . . 4 (∃𝑤𝑧((𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ ∃𝑤𝑧(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)))
63, 5bitr4i 278 . . 3 (∃𝑧𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)) ↔ ∃𝑤𝑧((𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
7 vex 3477 . . . . . . 7 𝑧 ∈ V
8 vex 3477 . . . . . . 7 𝑦 ∈ V
97, 8brco 5870 . . . . . 6 (𝑧(𝐴𝐵)𝑦 ↔ ∃𝑤(𝑧𝐵𝑤𝑤𝐴𝑦))
109anbi2i 622 . . . . 5 ((𝑥𝐶𝑧𝑧(𝐴𝐵)𝑦) ↔ (𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤𝑤𝐴𝑦)))
1110exbii 1849 . . . 4 (∃𝑧(𝑥𝐶𝑧𝑧(𝐴𝐵)𝑦) ↔ ∃𝑧(𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤𝑤𝐴𝑦)))
12 vex 3477 . . . . 5 𝑥 ∈ V
1312, 8opelco 5871 . . . 4 (⟨𝑥, 𝑦⟩ ∈ ((𝐴𝐵) ∘ 𝐶) ↔ ∃𝑧(𝑥𝐶𝑧𝑧(𝐴𝐵)𝑦))
14 exdistr 1957 . . . 4 (∃𝑧𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)) ↔ ∃𝑧(𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤𝑤𝐴𝑦)))
1511, 13, 143bitr4i 303 . . 3 (⟨𝑥, 𝑦⟩ ∈ ((𝐴𝐵) ∘ 𝐶) ↔ ∃𝑧𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)))
16 vex 3477 . . . . . . 7 𝑤 ∈ V
1712, 16brco 5870 . . . . . 6 (𝑥(𝐵𝐶)𝑤 ↔ ∃𝑧(𝑥𝐶𝑧𝑧𝐵𝑤))
1817anbi1i 623 . . . . 5 ((𝑥(𝐵𝐶)𝑤𝑤𝐴𝑦) ↔ (∃𝑧(𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
1918exbii 1849 . . . 4 (∃𝑤(𝑥(𝐵𝐶)𝑤𝑤𝐴𝑦) ↔ ∃𝑤(∃𝑧(𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
2012, 8opelco 5871 . . . 4 (⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ (𝐵𝐶)) ↔ ∃𝑤(𝑥(𝐵𝐶)𝑤𝑤𝐴𝑦))
21 19.41v 1952 . . . . 5 (∃𝑧((𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ (∃𝑧(𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
2221exbii 1849 . . . 4 (∃𝑤𝑧((𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ ∃𝑤(∃𝑧(𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
2319, 20, 223bitr4i 303 . . 3 (⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ (𝐵𝐶)) ↔ ∃𝑤𝑧((𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
246, 15, 233bitr4i 303 . 2 (⟨𝑥, 𝑦⟩ ∈ ((𝐴𝐵) ∘ 𝐶) ↔ ⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ (𝐵𝐶)))
251, 2, 24eqrelriiv 5790 1 ((𝐴𝐵) ∘ 𝐶) = (𝐴 ∘ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wa 395   = wceq 1540  wex 1780  wcel 2105  cop 4634   class class class wbr 5148  ccom 5680
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-11 2153  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-xp 5682  df-rel 5683  df-co 5685
This theorem is referenced by:  funcoeqres  6864  fcof1oinvd  7294  tposco  8248  mapen  9147  mapfien  9409  hashfacen  14420  hashfacenOLD  14421  relexpsucnnl  14984  relexpaddnn  15005  cofuass  17846  setccatid  18044  estrccatid  18093  frmdup3lem  18789  symggrplem  18807  f1omvdco2  19364  symggen  19386  psgnunilem1  19409  gsumval3  19823  gsumzf1o  19828  gsumzmhm  19853  prds1  20218  psrass1lemOLD  21803  psrass1lem  21806  pf1mpf  22191  pf1ind  22194  qtophmeo  23641  uniioombllem2  25432  cncombf  25507  motgrp  28228  pjsdi2i  31844  pjadj2coi  31891  pj3lem1  31893  pj3i  31895  fcoinver  32269  fmptco1f1o  32291  fcobij  32381  fcobijfs  32382  symgfcoeu  32680  pmtrcnel2  32688  cycpmconjv  32738  cycpmconjslem1  32750  cycpmconjs  32752  cyc3conja  32753  reprpmtf1o  34103  derangenlem  34627  subfacp1lem5  34640  erdsze2lem2  34660  pprodcnveq  35326  cocnv  37059  ltrncoidN  39465  trlcoabs2N  40059  trlcoat  40060  trlcone  40065  cdlemg46  40072  cdlemg47  40073  ltrnco4  40076  tgrpgrplem  40086  tendoplass  40120  cdlemi2  40156  cdlemk2  40169  cdlemk4  40171  cdlemk8  40175  cdlemk45  40284  cdlemk54  40295  cdlemk55a  40296  erngdvlem3  40327  erngdvlem3-rN  40335  tendocnv  40358  dvhvaddass  40434  dvhlveclem  40445  cdlemn8  40541  dihopelvalcpre  40585  dih1dimatlem0  40665  diophrw  41962  eldioph2  41965  mendring  42399  cortrcltrcl  42956  corclrtrcl  42957  cortrclrcl  42959  cotrclrtrcl  42960  cortrclrtrcl  42961  frege131d  42980  brcofffn  43247  brco3f1o  43249  neicvgnvo  43331  volicoff  45172  voliooicof  45173  ovolval4lem2  45827  isomushgr  46955  rngccatidALTV  47111  ringccatidALTV  47145
  Copyright terms: Public domain W3C validator