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

Theorem coass 6169
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 6148 . 2 Rel ((𝐴𝐵) ∘ 𝐶)
2 relco 6148 . 2 Rel (𝐴 ∘ (𝐵𝐶))
3 excom 2162 . . . 4 (∃𝑧𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)) ↔ ∃𝑤𝑧(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)))
4 anass 469 . . . . 5 (((𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ (𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)))
542exbii 1851 . . . 4 (∃𝑤𝑧((𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ ∃𝑤𝑧(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)))
63, 5bitr4i 277 . . 3 (∃𝑧𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)) ↔ ∃𝑤𝑧((𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
7 vex 3436 . . . . . . 7 𝑧 ∈ V
8 vex 3436 . . . . . . 7 𝑦 ∈ V
97, 8brco 5779 . . . . . 6 (𝑧(𝐴𝐵)𝑦 ↔ ∃𝑤(𝑧𝐵𝑤𝑤𝐴𝑦))
109anbi2i 623 . . . . 5 ((𝑥𝐶𝑧𝑧(𝐴𝐵)𝑦) ↔ (𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤𝑤𝐴𝑦)))
1110exbii 1850 . . . 4 (∃𝑧(𝑥𝐶𝑧𝑧(𝐴𝐵)𝑦) ↔ ∃𝑧(𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤𝑤𝐴𝑦)))
12 vex 3436 . . . . 5 𝑥 ∈ V
1312, 8opelco 5780 . . . 4 (⟨𝑥, 𝑦⟩ ∈ ((𝐴𝐵) ∘ 𝐶) ↔ ∃𝑧(𝑥𝐶𝑧𝑧(𝐴𝐵)𝑦))
14 exdistr 1958 . . . 4 (∃𝑧𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)) ↔ ∃𝑧(𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤𝑤𝐴𝑦)))
1511, 13, 143bitr4i 303 . . 3 (⟨𝑥, 𝑦⟩ ∈ ((𝐴𝐵) ∘ 𝐶) ↔ ∃𝑧𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)))
16 vex 3436 . . . . . . 7 𝑤 ∈ V
1712, 16brco 5779 . . . . . 6 (𝑥(𝐵𝐶)𝑤 ↔ ∃𝑧(𝑥𝐶𝑧𝑧𝐵𝑤))
1817anbi1i 624 . . . . 5 ((𝑥(𝐵𝐶)𝑤𝑤𝐴𝑦) ↔ (∃𝑧(𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
1918exbii 1850 . . . 4 (∃𝑤(𝑥(𝐵𝐶)𝑤𝑤𝐴𝑦) ↔ ∃𝑤(∃𝑧(𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
2012, 8opelco 5780 . . . 4 (⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ (𝐵𝐶)) ↔ ∃𝑤(𝑥(𝐵𝐶)𝑤𝑤𝐴𝑦))
21 19.41v 1953 . . . . 5 (∃𝑧((𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ (∃𝑧(𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
2221exbii 1850 . . . 4 (∃𝑤𝑧((𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ ∃𝑤(∃𝑧(𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
2319, 20, 223bitr4i 303 . . 3 (⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ (𝐵𝐶)) ↔ ∃𝑤𝑧((𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
246, 15, 233bitr4i 303 . 2 (⟨𝑥, 𝑦⟩ ∈ ((𝐴𝐵) ∘ 𝐶) ↔ ⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ (𝐵𝐶)))
251, 2, 24eqrelriiv 5700 1 ((𝐴𝐵) ∘ 𝐶) = (𝐴 ∘ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wa 396   = wceq 1539  wex 1782  wcel 2106  cop 4567   class class class wbr 5074  ccom 5593
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-11 2154  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-xp 5595  df-rel 5596  df-co 5598
This theorem is referenced by:  funcoeqres  6747  fcof1oinvd  7165  tposco  8073  mapen  8928  mapfien  9167  hashfacen  14166  hashfacenOLD  14167  relexpsucnnl  14741  relexpaddnn  14762  cofuass  17604  setccatid  17799  estrccatid  17848  frmdup3lem  18505  symggrplem  18523  f1omvdco2  19056  symggen  19078  psgnunilem1  19101  gsumval3  19508  gsumzf1o  19513  gsumzmhm  19538  prds1  19853  psrass1lemOLD  21143  psrass1lem  21146  pf1mpf  21518  pf1ind  21521  qtophmeo  22968  uniioombllem2  24747  cncombf  24822  motgrp  26904  pjsdi2i  30519  pjadj2coi  30566  pj3lem1  30568  pj3i  30570  fcoinver  30946  fmptco1f1o  30968  fcobij  31057  fcobijfs  31058  symgfcoeu  31351  pmtrcnel2  31359  cycpmconjv  31409  cycpmconjslem1  31421  cycpmconjs  31423  cyc3conja  31424  reprpmtf1o  32606  derangenlem  33133  subfacp1lem5  33146  erdsze2lem2  33166  pprodcnveq  34185  cocnv  35883  ltrncoidN  38142  trlcoabs2N  38736  trlcoat  38737  trlcone  38742  cdlemg46  38749  cdlemg47  38750  ltrnco4  38753  tgrpgrplem  38763  tendoplass  38797  cdlemi2  38833  cdlemk2  38846  cdlemk4  38848  cdlemk8  38852  cdlemk45  38961  cdlemk54  38972  cdlemk55a  38973  erngdvlem3  39004  erngdvlem3-rN  39012  tendocnv  39035  dvhvaddass  39111  dvhlveclem  39122  cdlemn8  39218  dihopelvalcpre  39262  dih1dimatlem0  39342  diophrw  40581  eldioph2  40584  mendring  41017  cortrcltrcl  41348  corclrtrcl  41349  cortrclrcl  41351  cotrclrtrcl  41352  cortrclrtrcl  41353  frege131d  41372  brcofffn  41641  brco3f1o  41643  neicvgnvo  41725  volicoff  43536  voliooicof  43537  ovolval4lem2  44188  isomushgr  45278  rngccatidALTV  45547  ringccatidALTV  45610
  Copyright terms: Public domain W3C validator