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

Theorem coass 5879
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 5858 . 2 Rel ((𝐴𝐵) ∘ 𝐶)
2 relco 5858 . 2 Rel (𝐴 ∘ (𝐵𝐶))
3 excom 2210 . . . 4 (∃𝑧𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)) ↔ ∃𝑤𝑧(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)))
4 anass 456 . . . . 5 (((𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ (𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)))
542exbii 1934 . . . 4 (∃𝑤𝑧((𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ ∃𝑤𝑧(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)))
63, 5bitr4i 269 . . 3 (∃𝑧𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)) ↔ ∃𝑤𝑧((𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
7 vex 3405 . . . . . . 7 𝑧 ∈ V
8 vex 3405 . . . . . . 7 𝑦 ∈ V
97, 8brco 5505 . . . . . 6 (𝑧(𝐴𝐵)𝑦 ↔ ∃𝑤(𝑧𝐵𝑤𝑤𝐴𝑦))
109anbi2i 611 . . . . 5 ((𝑥𝐶𝑧𝑧(𝐴𝐵)𝑦) ↔ (𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤𝑤𝐴𝑦)))
1110exbii 1933 . . . 4 (∃𝑧(𝑥𝐶𝑧𝑧(𝐴𝐵)𝑦) ↔ ∃𝑧(𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤𝑤𝐴𝑦)))
12 vex 3405 . . . . 5 𝑥 ∈ V
1312, 8opelco 5506 . . . 4 (⟨𝑥, 𝑦⟩ ∈ ((𝐴𝐵) ∘ 𝐶) ↔ ∃𝑧(𝑥𝐶𝑧𝑧(𝐴𝐵)𝑦))
14 exdistr 2045 . . . 4 (∃𝑧𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)) ↔ ∃𝑧(𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤𝑤𝐴𝑦)))
1511, 13, 143bitr4i 294 . . 3 (⟨𝑥, 𝑦⟩ ∈ ((𝐴𝐵) ∘ 𝐶) ↔ ∃𝑧𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)))
16 vex 3405 . . . . . . 7 𝑤 ∈ V
1712, 16brco 5505 . . . . . 6 (𝑥(𝐵𝐶)𝑤 ↔ ∃𝑧(𝑥𝐶𝑧𝑧𝐵𝑤))
1817anbi1i 612 . . . . 5 ((𝑥(𝐵𝐶)𝑤𝑤𝐴𝑦) ↔ (∃𝑧(𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
1918exbii 1933 . . . 4 (∃𝑤(𝑥(𝐵𝐶)𝑤𝑤𝐴𝑦) ↔ ∃𝑤(∃𝑧(𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
2012, 8opelco 5506 . . . 4 (⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ (𝐵𝐶)) ↔ ∃𝑤(𝑥(𝐵𝐶)𝑤𝑤𝐴𝑦))
21 19.41v 2040 . . . . 5 (∃𝑧((𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ (∃𝑧(𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
2221exbii 1933 . . . 4 (∃𝑤𝑧((𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ ∃𝑤(∃𝑧(𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
2319, 20, 223bitr4i 294 . . 3 (⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ (𝐵𝐶)) ↔ ∃𝑤𝑧((𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
246, 15, 233bitr4i 294 . 2 (⟨𝑥, 𝑦⟩ ∈ ((𝐴𝐵) ∘ 𝐶) ↔ ⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ (𝐵𝐶)))
251, 2, 24eqrelriiv 5427 1 ((𝐴𝐵) ∘ 𝐶) = (𝐴 ∘ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wa 384   = wceq 1637  wex 1859  wcel 2157  cop 4387   class class class wbr 4855  ccom 5326
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4986  ax-nul 4994  ax-pr 5107
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-rab 3116  df-v 3404  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-br 4856  df-opab 4918  df-xp 5328  df-rel 5329  df-co 5331
This theorem is referenced by:  funcoeqres  6390  fcof1oinvd  6779  tposco  7625  mapen  8370  mapfien  8559  hashfacen  13462  relexpsucnnl  14002  relexpaddnn  14021  cofuass  16760  setccatid  16945  estrccatid  16983  frmdup3lem  17615  symggrp  18028  f1omvdco2  18076  symggen  18098  psgnunilem1  18121  gsumval3  18516  gsumzf1o  18521  gsumzmhm  18545  prds1  18823  psrass1lem  19593  pf1mpf  19931  pf1ind  19934  qtophmeo  21842  uniioombllem2  23574  cncombf  23649  motgrp  25662  pjsdi2i  29354  pjadj2coi  29401  pj3lem1  29403  pj3i  29405  fcoinver  29753  fmptco1f1o  29771  fcobij  29837  fcobijfs  29838  symgfcoeu  30180  reprpmtf1o  31039  derangenlem  31485  subfacp1lem5  31498  erdsze2lem2  31518  pprodcnveq  32320  cocnv  33838  ltrncoidN  35914  trlcoabs2N  36508  trlcoat  36509  trlcone  36514  cdlemg46  36521  cdlemg47  36522  ltrnco4  36525  tgrpgrplem  36535  tendoplass  36569  cdlemi2  36605  cdlemk2  36618  cdlemk4  36620  cdlemk8  36624  cdlemk45  36733  cdlemk54  36744  cdlemk55a  36745  erngdvlem3  36776  erngdvlem3-rN  36784  tendocnv  36807  dvhvaddass  36883  dvhlveclem  36894  cdlemn8  36990  dihopelvalcpre  37034  dih1dimatlem0  37114  diophrw  37829  eldioph2  37832  mendring  38268  cortrcltrcl  38537  corclrtrcl  38538  cortrclrcl  38540  cotrclrtrcl  38541  cortrclrtrcl  38542  frege131d  38561  brcofffn  38834  brco3f1o  38836  neicvgnvo  38918  volicoff  40696  voliooicof  40697  ovolval4lem2  41351  rngccatidALTV  42562  ringccatidALTV  42625
  Copyright terms: Public domain W3C validator