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

Theorem cores 5340
Description: Restricted first member of a class composition. (Contributed by NM, 12-Oct-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
Assertion
Ref Expression
cores  |-  ( ran 
B  C_  C  ->  ( ( A  |`  C )  o.  B )  =  ( A  o.  B
) )

Proof of Theorem cores
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 2974 . . . . . . 7  |-  z  e. 
_V
2 vex 2974 . . . . . . 7  |-  y  e. 
_V
31, 2brelrn 5069 . . . . . 6  |-  ( z B y  ->  y  e.  ran  B )
4 ssel 3349 . . . . . 6  |-  ( ran 
B  C_  C  ->  ( y  e.  ran  B  ->  y  e.  C ) )
5 vex 2974 . . . . . . . 8  |-  x  e. 
_V
65brres 5116 . . . . . . 7  |-  ( y ( A  |`  C ) x  <->  ( y A x  /\  y  e.  C ) )
76rbaib 898 . . . . . 6  |-  ( y  e.  C  ->  (
y ( A  |`  C ) x  <->  y A x ) )
83, 4, 7syl56 34 . . . . 5  |-  ( ran 
B  C_  C  ->  ( z B y  -> 
( y ( A  |`  C ) x  <->  y A x ) ) )
98pm5.32d 639 . . . 4  |-  ( ran 
B  C_  C  ->  ( ( z B y  /\  y ( A  |`  C ) x )  <-> 
( z B y  /\  y A x ) ) )
109exbidv 1680 . . 3  |-  ( ran 
B  C_  C  ->  ( E. y ( z B y  /\  y
( A  |`  C ) x )  <->  E. y
( z B y  /\  y A x ) ) )
1110opabbidv 4354 . 2  |-  ( ran 
B  C_  C  ->  {
<. z ,  x >.  |  E. y ( z B y  /\  y
( A  |`  C ) x ) }  =  { <. z ,  x >.  |  E. y ( z B y  /\  y A x ) } )
12 df-co 4848 . 2  |-  ( ( A  |`  C )  o.  B )  =  { <. z ,  x >.  |  E. y ( z B y  /\  y
( A  |`  C ) x ) }
13 df-co 4848 . 2  |-  ( A  o.  B )  =  { <. z ,  x >.  |  E. y ( z B y  /\  y A x ) }
1411, 12, 133eqtr4g 2499 1  |-  ( ran 
B  C_  C  ->  ( ( A  |`  C )  o.  B )  =  ( A  o.  B
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1369   E.wex 1586    e. wcel 1756    C_ wss 3327   class class class wbr 4291   {copab 4348   ran crn 4840    |` cres 4841    o. ccom 4843
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 4412  ax-nul 4420  ax-pr 4530
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-eu 2257  df-mo 2258  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-ral 2719  df-rex 2720  df-rab 2723  df-v 2973  df-dif 3330  df-un 3332  df-in 3334  df-ss 3341  df-nul 3637  df-if 3791  df-sn 3877  df-pr 3879  df-op 3883  df-br 4292  df-opab 4350  df-xp 4845  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851
This theorem is referenced by:  cocnvcnv1  5347  cores2  5349  relcoi2  5364  fco2  5568  fcoi2  5585  domss2  7469  canthp1lem2  8819  imasdsval2  14453  frmdss2  15540  gsumval3OLD  16381  gsumval3lem1  16382  gsumzres  16387  gsumzresOLD  16391  gsumzaddlem  16407  gsumzaddlemOLD  16409  dprdf1  16529  kgencn2  19129  tsmsf1o  19718  hhssims  24675  eulerpartgbij  26754  lgamcvg2  27040  cvmlift2lem9a  27191  funresfunco  30029
  Copyright terms: Public domain W3C validator