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

Theorem resmpt2 6188
Description: Restriction of the mapping operation. (Contributed by Mario Carneiro, 17-Dec-2013.)
Assertion
Ref Expression
resmpt2  |-  ( ( C  C_  A  /\  D  C_  B )  -> 
( ( x  e.  A ,  y  e.  B  |->  E )  |`  ( C  X.  D
) )  =  ( x  e.  C , 
y  e.  D  |->  E ) )
Distinct variable groups:    x, A, y    x, B, y    x, C, y    x, D, y
Allowed substitution hints:    E( x, y)

Proof of Theorem resmpt2
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 resoprab2 6187 . 2  |-  ( ( C  C_  A  /\  D  C_  B )  -> 
( { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  E
) }  |`  ( C  X.  D ) )  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  C  /\  y  e.  D )  /\  z  =  E
) } )
2 df-mpt2 6096 . . 3  |-  ( x  e.  A ,  y  e.  B  |->  E )  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  E
) }
32reseq1i 5106 . 2  |-  ( ( x  e.  A , 
y  e.  B  |->  E )  |`  ( C  X.  D ) )  =  ( { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  E
) }  |`  ( C  X.  D ) )
4 df-mpt2 6096 . 2  |-  ( x  e.  C ,  y  e.  D  |->  E )  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  C  /\  y  e.  D )  /\  z  =  E
) }
51, 3, 43eqtr4g 2500 1  |-  ( ( C  C_  A  /\  D  C_  B )  -> 
( ( x  e.  A ,  y  e.  B  |->  E )  |`  ( C  X.  D
) )  =  ( x  e.  C , 
y  e.  D  |->  E ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369    e. wcel 1756    C_ wss 3328    X. cxp 4838    |` cres 4842   {coprab 6092    e. cmpt2 6093
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413  ax-nul 4421  ax-pr 4531
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-opab 4351  df-xp 4846  df-rel 4847  df-res 4852  df-oprab 6095  df-mpt2 6096
This theorem is referenced by:  ofmres  6573  cantnfval2  7877  cantnfval2OLD  7907  pgrpsubgsymg  15913  sylow3lem5  16130  mamures  18290  mdetrsca2  18411  mdetrlin2  18413  mdetunilem5  18422  smadiadetglem1  18477  smadiadetglem2  18478  txss12  19178  txbasval  19179  cnmpt2res  19250  fmucndlem  19866  cnmpt2pc  20500  oprpiece1res1  20523  oprpiece1res2  20524  cxpcn3  22186  ressplusf  26111  cvmlift2lem6  27197  cvmlift2lem12  27203
  Copyright terms: Public domain W3C validator