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

Theorem coass 6115
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 6094 . 2 Rel ((𝐴𝐵) ∘ 𝐶)
2 relco 6094 . 2 Rel (𝐴 ∘ (𝐵𝐶))
3 excom 2159 . . . 4 (∃𝑧𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)) ↔ ∃𝑤𝑧(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)))
4 anass 469 . . . . 5 (((𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ (𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)))
542exbii 1842 . . . 4 (∃𝑤𝑧((𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ ∃𝑤𝑧(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)))
63, 5bitr4i 279 . . 3 (∃𝑧𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)) ↔ ∃𝑤𝑧((𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
7 vex 3502 . . . . . . 7 𝑧 ∈ V
8 vex 3502 . . . . . . 7 𝑦 ∈ V
97, 8brco 5739 . . . . . 6 (𝑧(𝐴𝐵)𝑦 ↔ ∃𝑤(𝑧𝐵𝑤𝑤𝐴𝑦))
109anbi2i 622 . . . . 5 ((𝑥𝐶𝑧𝑧(𝐴𝐵)𝑦) ↔ (𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤𝑤𝐴𝑦)))
1110exbii 1841 . . . 4 (∃𝑧(𝑥𝐶𝑧𝑧(𝐴𝐵)𝑦) ↔ ∃𝑧(𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤𝑤𝐴𝑦)))
12 vex 3502 . . . . 5 𝑥 ∈ V
1312, 8opelco 5740 . . . 4 (⟨𝑥, 𝑦⟩ ∈ ((𝐴𝐵) ∘ 𝐶) ↔ ∃𝑧(𝑥𝐶𝑧𝑧(𝐴𝐵)𝑦))
14 exdistr 1948 . . . 4 (∃𝑧𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)) ↔ ∃𝑧(𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤𝑤𝐴𝑦)))
1511, 13, 143bitr4i 304 . . 3 (⟨𝑥, 𝑦⟩ ∈ ((𝐴𝐵) ∘ 𝐶) ↔ ∃𝑧𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)))
16 vex 3502 . . . . . . 7 𝑤 ∈ V
1712, 16brco 5739 . . . . . 6 (𝑥(𝐵𝐶)𝑤 ↔ ∃𝑧(𝑥𝐶𝑧𝑧𝐵𝑤))
1817anbi1i 623 . . . . 5 ((𝑥(𝐵𝐶)𝑤𝑤𝐴𝑦) ↔ (∃𝑧(𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
1918exbii 1841 . . . 4 (∃𝑤(𝑥(𝐵𝐶)𝑤𝑤𝐴𝑦) ↔ ∃𝑤(∃𝑧(𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
2012, 8opelco 5740 . . . 4 (⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ (𝐵𝐶)) ↔ ∃𝑤(𝑥(𝐵𝐶)𝑤𝑤𝐴𝑦))
21 19.41v 1943 . . . . 5 (∃𝑧((𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ (∃𝑧(𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
2221exbii 1841 . . . 4 (∃𝑤𝑧((𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ ∃𝑤(∃𝑧(𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
2319, 20, 223bitr4i 304 . . 3 (⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ (𝐵𝐶)) ↔ ∃𝑤𝑧((𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
246, 15, 233bitr4i 304 . 2 (⟨𝑥, 𝑦⟩ ∈ ((𝐴𝐵) ∘ 𝐶) ↔ ⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ (𝐵𝐶)))
251, 2, 24eqrelriiv 5661 1 ((𝐴𝐵) ∘ 𝐶) = (𝐴 ∘ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wa 396   = wceq 1530  wex 1773  wcel 2106  cop 4569   class class class wbr 5062  ccom 5557
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2152  ax-12 2167  ax-ext 2796  ax-sep 5199  ax-nul 5206  ax-pr 5325
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2615  df-eu 2649  df-clab 2803  df-cleq 2817  df-clel 2897  df-nfc 2967  df-rab 3151  df-v 3501  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-sn 4564  df-pr 4566  df-op 4570  df-br 5063  df-opab 5125  df-xp 5559  df-rel 5560  df-co 5562
This theorem is referenced by:  funcoeqres  6641  fcof1oinvd  7046  tposco  7917  mapen  8673  mapfien  8863  hashfacen  13805  relexpsucnnl  14384  relexpaddnn  14403  cofuass  17151  setccatid  17336  estrccatid  17374  frmdup3lem  18016  symggrp  18450  f1omvdco2  18498  symggen  18520  psgnunilem1  18543  gsumval3  18949  gsumzf1o  18954  gsumzmhm  18979  prds1  19286  psrass1lem  20078  pf1mpf  20431  pf1ind  20434  qtophmeo  22341  uniioombllem2  24099  cncombf  24174  motgrp  26243  pjsdi2i  29849  pjadj2coi  29896  pj3lem1  29898  pj3i  29900  fcoinver  30273  fmptco1f1o  30294  fcobij  30372  fcobijfs  30373  symgfcoeu  30641  pmtrcnel2  30649  cycpmconjv  30699  cycpmconjslem1  30711  cycpmconjs  30713  cyc3conja  30714  reprpmtf1o  31784  derangenlem  32303  subfacp1lem5  32316  erdsze2lem2  32336  pprodcnveq  33229  cocnv  34869  ltrncoidN  37132  trlcoabs2N  37726  trlcoat  37727  trlcone  37732  cdlemg46  37739  cdlemg47  37740  ltrnco4  37743  tgrpgrplem  37753  tendoplass  37787  cdlemi2  37823  cdlemk2  37836  cdlemk4  37838  cdlemk8  37842  cdlemk45  37951  cdlemk54  37962  cdlemk55a  37963  erngdvlem3  37994  erngdvlem3-rN  38002  tendocnv  38025  dvhvaddass  38101  dvhlveclem  38112  cdlemn8  38208  dihopelvalcpre  38252  dih1dimatlem0  38332  diophrw  39218  eldioph2  39221  mendring  39654  cortrcltrcl  39947  corclrtrcl  39948  cortrclrcl  39950  cotrclrtrcl  39951  cortrclrtrcl  39952  frege131d  39971  brcofffn  40243  brco3f1o  40245  neicvgnvo  40327  volicoff  42143  voliooicof  42144  ovolval4lem2  42795  isomushgr  43820  rngccatidALTV  44089  ringccatidALTV  44152
  Copyright terms: Public domain W3C validator