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

Theorem resco 5338
Description: Associative law for the restriction of a composition. (Contributed by NM, 12-Dec-2006.)
Assertion
Ref Expression
resco  |-  ( ( A  o.  B )  |`  C )  =  ( A  o.  ( B  |`  C ) )

Proof of Theorem resco
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relres 5131 . 2  |-  Rel  (
( A  o.  B
)  |`  C )
2 relco 5332 . 2  |-  Rel  ( A  o.  ( B  |`  C ) )
3 vex 3047 . . . . . 6  |-  x  e. 
_V
4 vex 3047 . . . . . 6  |-  y  e. 
_V
53, 4brco 5004 . . . . 5  |-  ( x ( A  o.  B
) y  <->  E. z
( x B z  /\  z A y ) )
65anbi1i 700 . . . 4  |-  ( ( x ( A  o.  B ) y  /\  x  e.  C )  <->  ( E. z ( x B z  /\  z A y )  /\  x  e.  C )
)
7 19.41v 1829 . . . 4  |-  ( E. z ( ( x B z  /\  z A y )  /\  x  e.  C )  <->  ( E. z ( x B z  /\  z A y )  /\  x  e.  C )
)
8 an32 806 . . . . . 6  |-  ( ( ( x B z  /\  z A y )  /\  x  e.  C )  <->  ( (
x B z  /\  x  e.  C )  /\  z A y ) )
9 vex 3047 . . . . . . . 8  |-  z  e. 
_V
109brres 5110 . . . . . . 7  |-  ( x ( B  |`  C ) z  <->  ( x B z  /\  x  e.  C ) )
1110anbi1i 700 . . . . . 6  |-  ( ( x ( B  |`  C ) z  /\  z A y )  <->  ( (
x B z  /\  x  e.  C )  /\  z A y ) )
128, 11bitr4i 256 . . . . 5  |-  ( ( ( x B z  /\  z A y )  /\  x  e.  C )  <->  ( x
( B  |`  C ) z  /\  z A y ) )
1312exbii 1717 . . . 4  |-  ( E. z ( ( x B z  /\  z A y )  /\  x  e.  C )  <->  E. z ( x ( B  |`  C )
z  /\  z A
y ) )
146, 7, 133bitr2i 277 . . 3  |-  ( ( x ( A  o.  B ) y  /\  x  e.  C )  <->  E. z ( x ( B  |`  C )
z  /\  z A
y ) )
154brres 5110 . . 3  |-  ( x ( ( A  o.  B )  |`  C ) y  <->  ( x ( A  o.  B ) y  /\  x  e.  C ) )
163, 4brco 5004 . . 3  |-  ( x ( A  o.  ( B  |`  C ) ) y  <->  E. z ( x ( B  |`  C ) z  /\  z A y ) )
1714, 15, 163bitr4i 281 . 2  |-  ( x ( ( A  o.  B )  |`  C ) y  <->  x ( A  o.  ( B  |`  C ) ) y )
181, 2, 17eqbrriv 4929 1  |-  ( ( A  o.  B )  |`  C )  =  ( A  o.  ( B  |`  C ) )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 371    = wceq 1443   E.wex 1662    e. wcel 1886   class class class wbr 4401    |` cres 4835    o. ccom 4837
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pr 4638
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-br 4402  df-opab 4461  df-xp 4839  df-rel 4840  df-co 4842  df-res 4845
This theorem is referenced by:  cocnvcnv2  5346  coires1  5352  relcoi1OLD  5364  dftpos2  6987  canthp1lem2  9075  o1res  13617  gsumzaddlem  17547  tsmsf1o  21152  tsmsmhm  21153  mbfres  22593  hhssims  26919  erdsze2lem2  29920  cvmlift2lem9a  30019  mbfresfi  31980  cocnv  32045  diophrw  35595  eldioph2  35598  mbfres2cn  37829  funcoressn  38622
  Copyright terms: Public domain W3C validator