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

Theorem resco 6270
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 6023 . 2 Rel ((𝐴𝐵) ↾ 𝐶)
2 relco 6126 . 2 Rel (𝐴 ∘ (𝐵𝐶))
3 vex 3484 . . . . . 6 𝑥 ∈ V
4 vex 3484 . . . . . 6 𝑦 ∈ V
53, 4brco 5881 . . . . 5 (𝑥(𝐴𝐵)𝑦 ↔ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦))
65anbi2i 623 . . . 4 ((𝑥𝐶𝑥(𝐴𝐵)𝑦) ↔ (𝑥𝐶 ∧ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)))
7 19.42v 1953 . . . 4 (∃𝑧(𝑥𝐶 ∧ (𝑥𝐵𝑧𝑧𝐴𝑦)) ↔ (𝑥𝐶 ∧ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)))
8 vex 3484 . . . . . . . 8 𝑧 ∈ V
98brresi 6006 . . . . . . 7 (𝑥(𝐵𝐶)𝑧 ↔ (𝑥𝐶𝑥𝐵𝑧))
109anbi1i 624 . . . . . 6 ((𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦) ↔ ((𝑥𝐶𝑥𝐵𝑧) ∧ 𝑧𝐴𝑦))
11 anass 468 . . . . . 6 (((𝑥𝐶𝑥𝐵𝑧) ∧ 𝑧𝐴𝑦) ↔ (𝑥𝐶 ∧ (𝑥𝐵𝑧𝑧𝐴𝑦)))
1210, 11bitr2i 276 . . . . 5 ((𝑥𝐶 ∧ (𝑥𝐵𝑧𝑧𝐴𝑦)) ↔ (𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦))
1312exbii 1848 . . . 4 (∃𝑧(𝑥𝐶 ∧ (𝑥𝐵𝑧𝑧𝐴𝑦)) ↔ ∃𝑧(𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦))
146, 7, 133bitr2i 299 . . 3 ((𝑥𝐶𝑥(𝐴𝐵)𝑦) ↔ ∃𝑧(𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦))
154brresi 6006 . . 3 (𝑥((𝐴𝐵) ↾ 𝐶)𝑦 ↔ (𝑥𝐶𝑥(𝐴𝐵)𝑦))
163, 4brco 5881 . . 3 (𝑥(𝐴 ∘ (𝐵𝐶))𝑦 ↔ ∃𝑧(𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦))
1714, 15, 163bitr4i 303 . 2 (𝑥((𝐴𝐵) ↾ 𝐶)𝑦𝑥(𝐴 ∘ (𝐵𝐶))𝑦)
181, 2, 17eqbrriv 5801 1 ((𝐴𝐵) ↾ 𝐶) = (𝐴 ∘ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wa 395   = wceq 1540  wex 1779  wcel 2108   class class class wbr 5143  cres 5687  ccom 5689
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-rel 5692  df-co 5694  df-res 5697
This theorem is referenced by:  cocnvcnv2  6278  coires1  6284  dftpos2  8268  ttrclco  9758  canthp1lem2  10693  o1res  15596  gsumzaddlem  19939  tsmsf1o  24153  tsmsmhm  24154  mbfres  25679  hhssims  31293  symgcom  33103  cycpmconjslem1  33174  cycpmconjslem2  33175  erdsze2lem2  35209  cvmlift2lem9a  35308  mbfresfi  37673  cocnv  37732  xrnres  38403  xrnres2  38404  xrnres3  38405  diophrw  42770  eldioph2  42773  mbfres2cn  45973  funcoressn  47054  tposrescnv  48779
  Copyright terms: Public domain W3C validator