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

Theorem relssres 5141
Description: Simplification law for restriction. (Contributed by NM, 16-Aug-1994.)
Assertion
Ref Expression
relssres  |-  ( ( Rel  A  /\  dom  A 
C_  B )  -> 
( A  |`  B )  =  A )

Proof of Theorem relssres
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 459 . . . 4  |-  ( ( Rel  A  /\  dom  A 
C_  B )  ->  Rel  A )
2 vex 3047 . . . . . . . . 9  |-  x  e. 
_V
3 vex 3047 . . . . . . . . 9  |-  y  e. 
_V
42, 3opeldm 5037 . . . . . . . 8  |-  ( <.
x ,  y >.  e.  A  ->  x  e. 
dom  A )
5 ssel 3425 . . . . . . . 8  |-  ( dom 
A  C_  B  ->  ( x  e.  dom  A  ->  x  e.  B ) )
64, 5syl5 33 . . . . . . 7  |-  ( dom 
A  C_  B  ->  (
<. x ,  y >.  e.  A  ->  x  e.  B ) )
76ancld 556 . . . . . 6  |-  ( dom 
A  C_  B  ->  (
<. x ,  y >.  e.  A  ->  ( <.
x ,  y >.  e.  A  /\  x  e.  B ) ) )
83opelres 5109 . . . . . 6  |-  ( <.
x ,  y >.  e.  ( A  |`  B )  <-> 
( <. x ,  y
>.  e.  A  /\  x  e.  B ) )
97, 8syl6ibr 231 . . . . 5  |-  ( dom 
A  C_  B  ->  (
<. x ,  y >.  e.  A  ->  <. x ,  y >.  e.  ( A  |`  B )
) )
109adantl 468 . . . 4  |-  ( ( Rel  A  /\  dom  A 
C_  B )  -> 
( <. x ,  y
>.  e.  A  ->  <. x ,  y >.  e.  ( A  |`  B )
) )
111, 10relssdv 4926 . . 3  |-  ( ( Rel  A  /\  dom  A 
C_  B )  ->  A  C_  ( A  |`  B ) )
12 resss 5127 . . 3  |-  ( A  |`  B )  C_  A
1311, 12jctil 540 . 2  |-  ( ( Rel  A  /\  dom  A 
C_  B )  -> 
( ( A  |`  B )  C_  A  /\  A  C_  ( A  |`  B ) ) )
14 eqss 3446 . 2  |-  ( ( A  |`  B )  =  A  <->  ( ( A  |`  B )  C_  A  /\  A  C_  ( A  |`  B ) ) )
1513, 14sylibr 216 1  |-  ( ( Rel  A  /\  dom  A 
C_  B )  -> 
( A  |`  B )  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    = wceq 1443    e. wcel 1886    C_ wss 3403   <.cop 3973   dom cdm 4833    |` cres 4835   Rel wrel 4838
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-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-dm 4843  df-res 4845
This theorem is referenced by:  resdm  5145  resid  5161  fnresdm  5683  f1ompt  6042  tfr2b  7111  tz7.48-2  7156  omxpenlem  7670  rankwflemb  8261  zorn2lem4  8926  relexpaddg  13109  setscom  15146  setsid  15157  dprd2da  17668  dprd2db  17669  ustssco  21222  dvres3  22861  dvres3a  22862  rlimcnp2  23885  constr3pthlem1  25376  ex-res  25884  nofulllem3  30586  nofulllem5  30588  poimirlem3  31936  relexpaddss  36304  fnresdmss  37425
  Copyright terms: Public domain W3C validator