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

Theorem setsid 13429
Description: Value of the structure replacement function at a replaced index. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
Hypothesis
Ref Expression
setsid.e  |-  E  = Slot  ( E `  ndx )
Assertion
Ref Expression
setsid  |-  ( ( W  e.  A  /\  C  e.  V )  ->  C  =  ( E `
 ( W sSet  <. ( E `  ndx ) ,  C >. ) ) )

Proof of Theorem setsid
StepHypRef Expression
1 setsval 13414 . . 3  |-  ( ( W  e.  A  /\  C  e.  V )  ->  ( W sSet  <. ( E `  ndx ) ,  C >. )  =  ( ( W  |`  ( _V  \  { ( E `
 ndx ) } ) )  u.  { <. ( E `  ndx ) ,  C >. } ) )
21fveq2d 5666 . 2  |-  ( ( W  e.  A  /\  C  e.  V )  ->  ( E `  ( W sSet  <. ( E `  ndx ) ,  C >. ) )  =  ( E `
 ( ( W  |`  ( _V  \  {
( E `  ndx ) } ) )  u. 
{ <. ( E `  ndx ) ,  C >. } ) ) )
3 setsid.e . . 3  |-  E  = Slot  ( E `  ndx )
4 resexg 5119 . . . . 5  |-  ( W  e.  A  ->  ( W  |`  ( _V  \  { ( E `  ndx ) } ) )  e.  _V )
54adantr 452 . . . 4  |-  ( ( W  e.  A  /\  C  e.  V )  ->  ( W  |`  ( _V  \  { ( E `
 ndx ) } ) )  e.  _V )
6 snex 4340 . . . 4  |-  { <. ( E `  ndx ) ,  C >. }  e.  _V
7 unexg 4644 . . . 4  |-  ( ( ( W  |`  ( _V  \  { ( E `
 ndx ) } ) )  e.  _V  /\ 
{ <. ( E `  ndx ) ,  C >. }  e.  _V )  -> 
( ( W  |`  ( _V  \  { ( E `  ndx ) } ) )  u. 
{ <. ( E `  ndx ) ,  C >. } )  e.  _V )
85, 6, 7sylancl 644 . . 3  |-  ( ( W  e.  A  /\  C  e.  V )  ->  ( ( W  |`  ( _V  \  { ( E `  ndx ) } ) )  u. 
{ <. ( E `  ndx ) ,  C >. } )  e.  _V )
93, 8strfvnd 13405 . 2  |-  ( ( W  e.  A  /\  C  e.  V )  ->  ( E `  (
( W  |`  ( _V  \  { ( E `
 ndx ) } ) )  u.  { <. ( E `  ndx ) ,  C >. } ) )  =  ( ( ( W  |`  ( _V  \  { ( E `  ndx ) } ) )  u. 
{ <. ( E `  ndx ) ,  C >. } ) `  ( E `
 ndx ) ) )
10 fvex 5676 . . . . . 6  |-  ( E `
 ndx )  e. 
_V
1110snid 3778 . . . . 5  |-  ( E `
 ndx )  e. 
{ ( E `  ndx ) }
12 fvres 5679 . . . . 5  |-  ( ( E `  ndx )  e.  { ( E `  ndx ) }  ->  (
( ( ( W  |`  ( _V  \  {
( E `  ndx ) } ) )  u. 
{ <. ( E `  ndx ) ,  C >. } )  |`  { ( E `  ndx ) } ) `  ( E `
 ndx ) )  =  ( ( ( W  |`  ( _V  \  { ( E `  ndx ) } ) )  u.  { <. ( E `  ndx ) ,  C >. } ) `  ( E `  ndx )
) )
1311, 12ax-mp 8 . . . 4  |-  ( ( ( ( W  |`  ( _V  \  { ( E `  ndx ) } ) )  u. 
{ <. ( E `  ndx ) ,  C >. } )  |`  { ( E `  ndx ) } ) `  ( E `
 ndx ) )  =  ( ( ( W  |`  ( _V  \  { ( E `  ndx ) } ) )  u.  { <. ( E `  ndx ) ,  C >. } ) `  ( E `  ndx )
)
14 resres 5093 . . . . . . . . 9  |-  ( ( W  |`  ( _V  \  { ( E `  ndx ) } ) )  |`  { ( E `  ndx ) } )  =  ( W  |`  (
( _V  \  {
( E `  ndx ) } )  i^i  {
( E `  ndx ) } ) )
15 incom 3470 . . . . . . . . . . . 12  |-  ( ( _V  \  { ( E `  ndx ) } )  i^i  {
( E `  ndx ) } )  =  ( { ( E `  ndx ) }  i^i  ( _V  \  { ( E `
 ndx ) } ) )
16 disjdif 3637 . . . . . . . . . . . 12  |-  ( { ( E `  ndx ) }  i^i  ( _V  \  { ( E `
 ndx ) } ) )  =  (/)
1715, 16eqtri 2401 . . . . . . . . . . 11  |-  ( ( _V  \  { ( E `  ndx ) } )  i^i  {
( E `  ndx ) } )  =  (/)
1817reseq2i 5077 . . . . . . . . . 10  |-  ( W  |`  ( ( _V  \  { ( E `  ndx ) } )  i^i 
{ ( E `  ndx ) } ) )  =  ( W  |`  (/) )
19 res0 5084 . . . . . . . . . 10  |-  ( W  |`  (/) )  =  (/)
2018, 19eqtri 2401 . . . . . . . . 9  |-  ( W  |`  ( ( _V  \  { ( E `  ndx ) } )  i^i 
{ ( E `  ndx ) } ) )  =  (/)
2114, 20eqtri 2401 . . . . . . . 8  |-  ( ( W  |`  ( _V  \  { ( E `  ndx ) } ) )  |`  { ( E `  ndx ) } )  =  (/)
2221a1i 11 . . . . . . 7  |-  ( ( W  e.  A  /\  C  e.  V )  ->  ( ( W  |`  ( _V  \  { ( E `  ndx ) } ) )  |`  { ( E `  ndx ) } )  =  (/) )
23 elex 2901 . . . . . . . . . . 11  |-  ( C  e.  V  ->  C  e.  _V )
2423adantl 453 . . . . . . . . . 10  |-  ( ( W  e.  A  /\  C  e.  V )  ->  C  e.  _V )
25 opelxpi 4844 . . . . . . . . . 10  |-  ( ( ( E `  ndx )  e.  _V  /\  C  e.  _V )  ->  <. ( E `  ndx ) ,  C >.  e.  ( _V  X.  _V ) )
2610, 24, 25sylancr 645 . . . . . . . . 9  |-  ( ( W  e.  A  /\  C  e.  V )  -> 
<. ( E `  ndx ) ,  C >.  e.  ( _V  X.  _V ) )
27 opex 4362 . . . . . . . . . 10  |-  <. ( E `  ndx ) ,  C >.  e.  _V
2827relsn 4913 . . . . . . . . 9  |-  ( Rel 
{ <. ( E `  ndx ) ,  C >. }  <->  <. ( E `  ndx ) ,  C >.  e.  ( _V  X.  _V ) )
2926, 28sylibr 204 . . . . . . . 8  |-  ( ( W  e.  A  /\  C  e.  V )  ->  Rel  { <. ( E `  ndx ) ,  C >. } )
30 dmsnopss 5276 . . . . . . . 8  |-  dom  { <. ( E `  ndx ) ,  C >. } 
C_  { ( E `
 ndx ) }
31 relssres 5117 . . . . . . . 8  |-  ( ( Rel  { <. ( E `  ndx ) ,  C >. }  /\  dom  {
<. ( E `  ndx ) ,  C >. } 
C_  { ( E `
 ndx ) } )  ->  ( { <. ( E `  ndx ) ,  C >. }  |`  { ( E `  ndx ) } )  =  { <. ( E `  ndx ) ,  C >. } )
3229, 30, 31sylancl 644 . . . . . . 7  |-  ( ( W  e.  A  /\  C  e.  V )  ->  ( { <. ( E `  ndx ) ,  C >. }  |`  { ( E `  ndx ) } )  =  { <. ( E `  ndx ) ,  C >. } )
3322, 32uneq12d 3439 . . . . . 6  |-  ( ( W  e.  A  /\  C  e.  V )  ->  ( ( ( W  |`  ( _V  \  {
( E `  ndx ) } ) )  |`  { ( E `  ndx ) } )  u.  ( { <. ( E `  ndx ) ,  C >. }  |`  { ( E `  ndx ) } ) )  =  ( (/)  u.  { <. ( E `  ndx ) ,  C >. } ) )
34 resundir 5095 . . . . . 6  |-  ( ( ( W  |`  ( _V  \  { ( E `
 ndx ) } ) )  u.  { <. ( E `  ndx ) ,  C >. } )  |`  { ( E `  ndx ) } )  =  ( ( ( W  |`  ( _V  \  { ( E `
 ndx ) } ) )  |`  { ( E `  ndx ) } )  u.  ( { <. ( E `  ndx ) ,  C >. }  |`  { ( E `  ndx ) } ) )
35 un0 3589 . . . . . . 7  |-  ( {
<. ( E `  ndx ) ,  C >. }  u.  (/) )  =  { <. ( E `  ndx ) ,  C >. }
36 uncom 3428 . . . . . . 7  |-  ( {
<. ( E `  ndx ) ,  C >. }  u.  (/) )  =  (
(/)  u.  { <. ( E `  ndx ) ,  C >. } )
3735, 36eqtr3i 2403 . . . . . 6  |-  { <. ( E `  ndx ) ,  C >. }  =  (
(/)  u.  { <. ( E `  ndx ) ,  C >. } )
3833, 34, 373eqtr4g 2438 . . . . 5  |-  ( ( W  e.  A  /\  C  e.  V )  ->  ( ( ( W  |`  ( _V  \  {
( E `  ndx ) } ) )  u. 
{ <. ( E `  ndx ) ,  C >. } )  |`  { ( E `  ndx ) } )  =  { <. ( E `  ndx ) ,  C >. } )
3938fveq1d 5664 . . . 4  |-  ( ( W  e.  A  /\  C  e.  V )  ->  ( ( ( ( W  |`  ( _V  \  { ( E `  ndx ) } ) )  u.  { <. ( E `  ndx ) ,  C >. } )  |`  { ( E `  ndx ) } ) `  ( E `  ndx )
)  =  ( {
<. ( E `  ndx ) ,  C >. } `
 ( E `  ndx ) ) )
4013, 39syl5eqr 2427 . . 3  |-  ( ( W  e.  A  /\  C  e.  V )  ->  ( ( ( W  |`  ( _V  \  {
( E `  ndx ) } ) )  u. 
{ <. ( E `  ndx ) ,  C >. } ) `  ( E `
 ndx ) )  =  ( { <. ( E `  ndx ) ,  C >. } `  ( E `  ndx ) ) )
4110a1i 11 . . . 4  |-  ( ( W  e.  A  /\  C  e.  V )  ->  ( E `  ndx )  e.  _V )
42 fvsng 5860 . . . 4  |-  ( ( ( E `  ndx )  e.  _V  /\  C  e.  V )  ->  ( { <. ( E `  ndx ) ,  C >. } `
 ( E `  ndx ) )  =  C )
4341, 42sylancom 649 . . 3  |-  ( ( W  e.  A  /\  C  e.  V )  ->  ( { <. ( E `  ndx ) ,  C >. } `  ( E `  ndx ) )  =  C )
4440, 43eqtrd 2413 . 2  |-  ( ( W  e.  A  /\  C  e.  V )  ->  ( ( ( W  |`  ( _V  \  {
( E `  ndx ) } ) )  u. 
{ <. ( E `  ndx ) ,  C >. } ) `  ( E `
 ndx ) )  =  C )
452, 9, 443eqtrrd 2418 1  |-  ( ( W  e.  A  /\  C  e.  V )  ->  C  =  ( E `
 ( W sSet  <. ( E `  ndx ) ,  C >. ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    e. wcel 1717   _Vcvv 2893    \ cdif 3254    u. cun 3255    i^i cin 3256    C_ wss 3257   (/)c0 3565   {csn 3751   <.cop 3754    X. cxp 4810   dom cdm 4812    |` cres 4814   Rel wrel 4817   ` cfv 5388  (class class class)co 6014   ndxcnx 13387   sSet csts 13388  Slot cslot 13389
This theorem is referenced by:  ressbas  13440  oppchomfval  13861  oppccofval  13863  reschom  13951  oduleval  14479  oppgplusfval  15065  mgpplusg  15573  opprmulfval  15651  srasca  16174  sravsca  16175  opsrle  16457  zlmsca  16719  zlmvsca  16720  znle  16734  thloc  16843  tuslem  18212  setsmstset  18391  tngds  18554  tngtset  18555  matmulr  27130  hlhilnvl  32120
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2362  ax-sep 4265  ax-nul 4273  ax-pr 4338  ax-un 4635
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2236  df-mo 2237  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2506  df-ne 2546  df-ral 2648  df-rex 2649  df-rab 2652  df-v 2895  df-sbc 3099  df-dif 3260  df-un 3262  df-in 3264  df-ss 3271  df-nul 3566  df-if 3677  df-sn 3757  df-pr 3758  df-op 3760  df-uni 3952  df-br 4148  df-opab 4202  df-mpt 4203  df-id 4433  df-xp 4818  df-rel 4819  df-cnv 4820  df-co 4821  df-dm 4822  df-res 4824  df-iota 5352  df-fun 5390  df-fv 5396  df-ov 6017  df-oprab 6018  df-mpt2 6019  df-slot 13394  df-sets 13396
  Copyright terms: Public domain W3C validator