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

Theorem resco 6075
 Description: Associative law for the restriction of a composition. (Contributed by NM, 12-Dec-2006.)
Assertion
Ref Expression
resco ((𝐴𝐵) ↾ 𝐶) = (𝐴 ∘ (𝐵𝐶))

Proof of Theorem resco
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relres 5850 . 2 Rel ((𝐴𝐵) ↾ 𝐶)
2 relco 6069 . 2 Rel (𝐴 ∘ (𝐵𝐶))
3 vex 3444 . . . . . 6 𝑥 ∈ V
4 vex 3444 . . . . . 6 𝑦 ∈ V
53, 4brco 5708 . . . . 5 (𝑥(𝐴𝐵)𝑦 ↔ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦))
65anbi2i 625 . . . 4 ((𝑥𝐶𝑥(𝐴𝐵)𝑦) ↔ (𝑥𝐶 ∧ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)))
7 19.42v 1954 . . . 4 (∃𝑧(𝑥𝐶 ∧ (𝑥𝐵𝑧𝑧𝐴𝑦)) ↔ (𝑥𝐶 ∧ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)))
8 vex 3444 . . . . . . . 8 𝑧 ∈ V
98brresi 5830 . . . . . . 7 (𝑥(𝐵𝐶)𝑧 ↔ (𝑥𝐶𝑥𝐵𝑧))
109anbi1i 626 . . . . . 6 ((𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦) ↔ ((𝑥𝐶𝑥𝐵𝑧) ∧ 𝑧𝐴𝑦))
11 anass 472 . . . . . 6 (((𝑥𝐶𝑥𝐵𝑧) ∧ 𝑧𝐴𝑦) ↔ (𝑥𝐶 ∧ (𝑥𝐵𝑧𝑧𝐴𝑦)))
1210, 11bitr2i 279 . . . . 5 ((𝑥𝐶 ∧ (𝑥𝐵𝑧𝑧𝐴𝑦)) ↔ (𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦))
1312exbii 1849 . . . 4 (∃𝑧(𝑥𝐶 ∧ (𝑥𝐵𝑧𝑧𝐴𝑦)) ↔ ∃𝑧(𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦))
146, 7, 133bitr2i 302 . . 3 ((𝑥𝐶𝑥(𝐴𝐵)𝑦) ↔ ∃𝑧(𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦))
154brresi 5830 . . 3 (𝑥((𝐴𝐵) ↾ 𝐶)𝑦 ↔ (𝑥𝐶𝑥(𝐴𝐵)𝑦))
163, 4brco 5708 . . 3 (𝑥(𝐴 ∘ (𝐵𝐶))𝑦 ↔ ∃𝑧(𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦))
1714, 15, 163bitr4i 306 . 2 (𝑥((𝐴𝐵) ↾ 𝐶)𝑦𝑥(𝐴 ∘ (𝐵𝐶))𝑦)
181, 2, 17eqbrriv 5631 1 ((𝐴𝐵) ↾ 𝐶) = (𝐴 ∘ (𝐵𝐶))
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111   class class class wbr 5033   ↾ cres 5524   ∘ ccom 5526 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5170  ax-nul 5177  ax-pr 5298 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-dif 3885  df-un 3887  df-in 3889  df-ss 3899  df-nul 4246  df-if 4428  df-sn 4528  df-pr 4530  df-op 4534  df-br 5034  df-opab 5096  df-xp 5528  df-rel 5529  df-co 5531  df-res 5534 This theorem is referenced by:  cocnvcnv2  6083  coires1  6089  dftpos2  7907  canthp1lem2  10079  o1res  14926  gsumzaddlem  19052  tsmsf1o  22788  tsmsmhm  22789  mbfres  24286  hhssims  29098  symgcom  30823  cycpmconjslem1  30892  cycpmconjslem2  30893  erdsze2lem2  32627  cvmlift2lem9a  32726  mbfresfi  35170  cocnv  35230  xrnres  35877  xrnres2  35878  xrnres3  35879  diophrw  39787  eldioph2  39790  mbfres2cn  42684  funcoressn  43718
 Copyright terms: Public domain W3C validator