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

Theorem resco 6207
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 5971 . 2 Rel ((𝐴𝐵) ↾ 𝐶)
2 relco 6065 . 2 Rel (𝐴 ∘ (𝐵𝐶))
3 vex 3452 . . . . . 6 𝑥 ∈ V
4 vex 3452 . . . . . 6 𝑦 ∈ V
53, 4brco 5831 . . . . 5 (𝑥(𝐴𝐵)𝑦 ↔ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦))
65anbi2i 624 . . . 4 ((𝑥𝐶𝑥(𝐴𝐵)𝑦) ↔ (𝑥𝐶 ∧ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)))
7 19.42v 1958 . . . 4 (∃𝑧(𝑥𝐶 ∧ (𝑥𝐵𝑧𝑧𝐴𝑦)) ↔ (𝑥𝐶 ∧ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦)))
8 vex 3452 . . . . . . . 8 𝑧 ∈ V
98brresi 5951 . . . . . . 7 (𝑥(𝐵𝐶)𝑧 ↔ (𝑥𝐶𝑥𝐵𝑧))
109anbi1i 625 . . . . . 6 ((𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦) ↔ ((𝑥𝐶𝑥𝐵𝑧) ∧ 𝑧𝐴𝑦))
11 anass 470 . . . . . 6 (((𝑥𝐶𝑥𝐵𝑧) ∧ 𝑧𝐴𝑦) ↔ (𝑥𝐶 ∧ (𝑥𝐵𝑧𝑧𝐴𝑦)))
1210, 11bitr2i 276 . . . . 5 ((𝑥𝐶 ∧ (𝑥𝐵𝑧𝑧𝐴𝑦)) ↔ (𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦))
1312exbii 1851 . . . 4 (∃𝑧(𝑥𝐶 ∧ (𝑥𝐵𝑧𝑧𝐴𝑦)) ↔ ∃𝑧(𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦))
146, 7, 133bitr2i 299 . . 3 ((𝑥𝐶𝑥(𝐴𝐵)𝑦) ↔ ∃𝑧(𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦))
154brresi 5951 . . 3 (𝑥((𝐴𝐵) ↾ 𝐶)𝑦 ↔ (𝑥𝐶𝑥(𝐴𝐵)𝑦))
163, 4brco 5831 . . 3 (𝑥(𝐴 ∘ (𝐵𝐶))𝑦 ↔ ∃𝑧(𝑥(𝐵𝐶)𝑧𝑧𝐴𝑦))
1714, 15, 163bitr4i 303 . 2 (𝑥((𝐴𝐵) ↾ 𝐶)𝑦𝑥(𝐴 ∘ (𝐵𝐶))𝑦)
181, 2, 17eqbrriv 5752 1 ((𝐴𝐵) ↾ 𝐶) = (𝐴 ∘ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wa 397   = wceq 1542  wex 1782  wcel 2107   class class class wbr 5110  cres 5640  ccom 5642
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pr 5389
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5173  df-xp 5644  df-rel 5645  df-co 5647  df-res 5650
This theorem is referenced by:  cocnvcnv2  6215  coires1  6221  dftpos2  8179  ttrclco  9661  canthp1lem2  10596  o1res  15449  gsumzaddlem  19705  tsmsf1o  23512  tsmsmhm  23513  mbfres  25024  hhssims  30258  symgcom  31976  cycpmconjslem1  32045  cycpmconjslem2  32046  erdsze2lem2  33838  cvmlift2lem9a  33937  mbfresfi  36153  cocnv  36213  xrnres  36893  xrnres2  36894  xrnres3  36895  diophrw  41111  eldioph2  41114  mbfres2cn  44273  funcoressn  45350
  Copyright terms: Public domain W3C validator