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

Theorem coass 5461
 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 5440 . 2 Rel ((𝐴𝐵) ∘ 𝐶)
2 relco 5440 . 2 Rel (𝐴 ∘ (𝐵𝐶))
3 excom 1978 . . . 4 (∃𝑧𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)) ↔ ∃𝑤𝑧(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)))
4 anass 678 . . . . 5 (((𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ (𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)))
542exbii 1753 . . . 4 (∃𝑤𝑧((𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ ∃𝑤𝑧(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)))
63, 5bitr4i 265 . . 3 (∃𝑧𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)) ↔ ∃𝑤𝑧((𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
7 vex 3080 . . . . . . 7 𝑧 ∈ V
8 vex 3080 . . . . . . 7 𝑦 ∈ V
97, 8brco 5106 . . . . . 6 (𝑧(𝐴𝐵)𝑦 ↔ ∃𝑤(𝑧𝐵𝑤𝑤𝐴𝑦))
109anbi2i 725 . . . . 5 ((𝑥𝐶𝑧𝑧(𝐴𝐵)𝑦) ↔ (𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤𝑤𝐴𝑦)))
1110exbii 1752 . . . 4 (∃𝑧(𝑥𝐶𝑧𝑧(𝐴𝐵)𝑦) ↔ ∃𝑧(𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤𝑤𝐴𝑦)))
12 vex 3080 . . . . 5 𝑥 ∈ V
1312, 8opelco 5107 . . . 4 (⟨𝑥, 𝑦⟩ ∈ ((𝐴𝐵) ∘ 𝐶) ↔ ∃𝑧(𝑥𝐶𝑧𝑧(𝐴𝐵)𝑦))
14 exdistr 1869 . . . 4 (∃𝑧𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)) ↔ ∃𝑧(𝑥𝐶𝑧 ∧ ∃𝑤(𝑧𝐵𝑤𝑤𝐴𝑦)))
1511, 13, 143bitr4i 290 . . 3 (⟨𝑥, 𝑦⟩ ∈ ((𝐴𝐵) ∘ 𝐶) ↔ ∃𝑧𝑤(𝑥𝐶𝑧 ∧ (𝑧𝐵𝑤𝑤𝐴𝑦)))
16 vex 3080 . . . . . . 7 𝑤 ∈ V
1712, 16brco 5106 . . . . . 6 (𝑥(𝐵𝐶)𝑤 ↔ ∃𝑧(𝑥𝐶𝑧𝑧𝐵𝑤))
1817anbi1i 726 . . . . 5 ((𝑥(𝐵𝐶)𝑤𝑤𝐴𝑦) ↔ (∃𝑧(𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
1918exbii 1752 . . . 4 (∃𝑤(𝑥(𝐵𝐶)𝑤𝑤𝐴𝑦) ↔ ∃𝑤(∃𝑧(𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
2012, 8opelco 5107 . . . 4 (⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ (𝐵𝐶)) ↔ ∃𝑤(𝑥(𝐵𝐶)𝑤𝑤𝐴𝑦))
21 19.41v 1864 . . . . 5 (∃𝑧((𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ (∃𝑧(𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
2221exbii 1752 . . . 4 (∃𝑤𝑧((𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦) ↔ ∃𝑤(∃𝑧(𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
2319, 20, 223bitr4i 290 . . 3 (⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ (𝐵𝐶)) ↔ ∃𝑤𝑧((𝑥𝐶𝑧𝑧𝐵𝑤) ∧ 𝑤𝐴𝑦))
246, 15, 233bitr4i 290 . 2 (⟨𝑥, 𝑦⟩ ∈ ((𝐴𝐵) ∘ 𝐶) ↔ ⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ (𝐵𝐶)))
251, 2, 24eqrelriiv 5030 1 ((𝐴𝐵) ∘ 𝐶) = (𝐴 ∘ (𝐵𝐶))
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 382   = wceq 1474  ∃wex 1694   ∈ wcel 1938  ⟨cop 4034   class class class wbr 4481   ∘ ccom 4936 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pr 4732 This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3079  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-nul 3778  df-if 3940  df-sn 4029  df-pr 4031  df-op 4035  df-br 4482  df-opab 4542  df-xp 4938  df-rel 4939  df-co 4941 This theorem is referenced by:  funcoeqres  5963  fcof1oinvd  6324  tposco  7144  mapen  7884  mapfien  8071  hashfacen  12958  relexpsucnnl  13477  relexpaddnn  13496  cofuass  16262  setccatid  16447  estrccatid  16485  frmdup3lem  17116  symggrp  17533  f1omvdco2  17581  symggen  17603  psgnunilem1  17626  gsumval3  18036  gsumzf1o  18041  gsumzmhm  18065  prds1  18342  psrass1lem  19100  pf1mpf  19439  pf1ind  19442  qtophmeo  21331  uniioombllem2  23033  cncombf  23107  motgrp  25129  pjsdi2i  28189  pjadj2coi  28236  pj3lem1  28238  pj3i  28240  fcoinver  28587  fcobij  28677  fcobijfs  28678  symgfcoeu  28973  derangenlem  30253  subfacp1lem5  30266  erdsze2lem2  30286  pprodcnveq  30996  cocnv  32565  ltrncoidN  34307  trlcoabs2N  34903  trlcoat  34904  trlcone  34909  cdlemg46  34916  cdlemg47  34917  ltrnco4  34920  tgrpgrplem  34930  tendoplass  34964  cdlemi2  35000  cdlemk2  35013  cdlemk4  35015  cdlemk8  35019  cdlemk45  35128  cdlemk54  35139  cdlemk55a  35140  erngdvlem3  35171  erngdvlem3-rN  35179  tendocnv  35203  dvhvaddass  35279  dvhlveclem  35290  cdlemn8  35386  dihopelvalcpre  35430  dih1dimatlem0  35510  diophrw  36215  eldioph2  36218  mendring  36663  cortrcltrcl  36933  corclrtrcl  36934  cortrclrcl  36936  cotrclrtrcl  36937  cortrclrtrcl  36938  frege131d  36957  brcofffn  37231  brco3f1o  37233  neicvgnvo  37315  volicoff  38778  voliooicof  38779  ovolval4lem2  39434  rngccatidALTV  41873  ringccatidALTV  41936
 Copyright terms: Public domain W3C validator