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

Theorem setsid 15102
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 15084 . . 3  |-  ( ( W  e.  A  /\  C  e.  V )  ->  ( W sSet  <. ( E `  ndx ) ,  C >. )  =  ( ( W  |`  ( _V  \  { ( E `
 ndx ) } ) )  u.  { <. ( E `  ndx ) ,  C >. } ) )
21fveq2d 5824 . 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 5104 . . . . 5  |-  ( W  e.  A  ->  ( W  |`  ( _V  \  { ( E `  ndx ) } ) )  e.  _V )
54adantr 466 . . . 4  |-  ( ( W  e.  A  /\  C  e.  V )  ->  ( W  |`  ( _V  \  { ( E `
 ndx ) } ) )  e.  _V )
6 snex 4600 . . . 4  |-  { <. ( E `  ndx ) ,  C >. }  e.  _V
7 unexg 6545 . . . 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 666 . . 3  |-  ( ( W  e.  A  /\  C  e.  V )  ->  ( ( W  |`  ( _V  \  { ( E `  ndx ) } ) )  u. 
{ <. ( E `  ndx ) ,  C >. } )  e.  _V )
93, 8strfvnd 15074 . 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 5830 . . . . . 6  |-  ( E `
 ndx )  e. 
_V
1110snid 3964 . . . . 5  |-  ( E `
 ndx )  e. 
{ ( E `  ndx ) }
12 fvres 5834 . . . . 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 5 . . . 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 5074 . . . . . . . . 9  |-  ( ( W  |`  ( _V  \  { ( E `  ndx ) } ) )  |`  { ( E `  ndx ) } )  =  ( W  |`  (
( _V  \  {
( E `  ndx ) } )  i^i  {
( E `  ndx ) } ) )
15 incom 3593 . . . . . . . . . . . 12  |-  ( ( _V  \  { ( E `  ndx ) } )  i^i  {
( E `  ndx ) } )  =  ( { ( E `  ndx ) }  i^i  ( _V  \  { ( E `
 ndx ) } ) )
16 disjdif 3807 . . . . . . . . . . . 12  |-  ( { ( E `  ndx ) }  i^i  ( _V  \  { ( E `
 ndx ) } ) )  =  (/)
1715, 16eqtri 2445 . . . . . . . . . . 11  |-  ( ( _V  \  { ( E `  ndx ) } )  i^i  {
( E `  ndx ) } )  =  (/)
1817reseq2i 5059 . . . . . . . . . 10  |-  ( W  |`  ( ( _V  \  { ( E `  ndx ) } )  i^i 
{ ( E `  ndx ) } ) )  =  ( W  |`  (/) )
19 res0 5066 . . . . . . . . . 10  |-  ( W  |`  (/) )  =  (/)
2018, 19eqtri 2445 . . . . . . . . 9  |-  ( W  |`  ( ( _V  \  { ( E `  ndx ) } )  i^i 
{ ( E `  ndx ) } ) )  =  (/)
2114, 20eqtri 2445 . . . . . . . 8  |-  ( ( W  |`  ( _V  \  { ( E `  ndx ) } ) )  |`  { ( E `  ndx ) } )  =  (/)
2221a1i 11 . . . . . . 7  |-  ( ( W  e.  A  /\  C  e.  V )  ->  ( ( W  |`  ( _V  \  { ( E `  ndx ) } ) )  |`  { ( E `  ndx ) } )  =  (/) )
23 elex 3026 . . . . . . . . . . 11  |-  ( C  e.  V  ->  C  e.  _V )
2423adantl 467 . . . . . . . . . 10  |-  ( ( W  e.  A  /\  C  e.  V )  ->  C  e.  _V )
25 opelxpi 4823 . . . . . . . . . 10  |-  ( ( ( E `  ndx )  e.  _V  /\  C  e.  _V )  ->  <. ( E `  ndx ) ,  C >.  e.  ( _V  X.  _V ) )
2610, 24, 25sylancr 667 . . . . . . . . 9  |-  ( ( W  e.  A  /\  C  e.  V )  -> 
<. ( E `  ndx ) ,  C >.  e.  ( _V  X.  _V ) )
27 opex 4623 . . . . . . . . . 10  |-  <. ( E `  ndx ) ,  C >.  e.  _V
2827relsn 4895 . . . . . . . . 9  |-  ( Rel 
{ <. ( E `  ndx ) ,  C >. }  <->  <. ( E `  ndx ) ,  C >.  e.  ( _V  X.  _V ) )
2926, 28sylibr 215 . . . . . . . 8  |-  ( ( W  e.  A  /\  C  e.  V )  ->  Rel  { <. ( E `  ndx ) ,  C >. } )
30 dmsnopss 5265 . . . . . . . 8  |-  dom  { <. ( E `  ndx ) ,  C >. } 
C_  { ( E `
 ndx ) }
31 relssres 5099 . . . . . . . 8  |-  ( ( Rel  { <. ( E `  ndx ) ,  C >. }  /\  dom  {
<. ( E `  ndx ) ,  C >. } 
C_  { ( E `
 ndx ) } )  ->  ( { <. ( E `  ndx ) ,  C >. }  |`  { ( E `  ndx ) } )  =  { <. ( E `  ndx ) ,  C >. } )
3229, 30, 31sylancl 666 . . . . . . 7  |-  ( ( W  e.  A  /\  C  e.  V )  ->  ( { <. ( E `  ndx ) ,  C >. }  |`  { ( E `  ndx ) } )  =  { <. ( E `  ndx ) ,  C >. } )
3322, 32uneq12d 3559 . . . . . 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 5076 . . . . . 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 3727 . . . . . . 7  |-  ( {
<. ( E `  ndx ) ,  C >. }  u.  (/) )  =  { <. ( E `  ndx ) ,  C >. }
36 uncom 3548 . . . . . . 7  |-  ( {
<. ( E `  ndx ) ,  C >. }  u.  (/) )  =  (
(/)  u.  { <. ( E `  ndx ) ,  C >. } )
3735, 36eqtr3i 2447 . . . . . 6  |-  { <. ( E `  ndx ) ,  C >. }  =  (
(/)  u.  { <. ( E `  ndx ) ,  C >. } )
3833, 34, 373eqtr4g 2482 . . . . 5  |-  ( ( W  e.  A  /\  C  e.  V )  ->  ( ( ( W  |`  ( _V  \  {
( E `  ndx ) } ) )  u. 
{ <. ( E `  ndx ) ,  C >. } )  |`  { ( E `  ndx ) } )  =  { <. ( E `  ndx ) ,  C >. } )
3938fveq1d 5822 . . . 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 2471 . . 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 6052 . . . 4  |-  ( ( ( E `  ndx )  e.  _V  /\  C  e.  V )  ->  ( { <. ( E `  ndx ) ,  C >. } `
 ( E `  ndx ) )  =  C )
4341, 42sylancom 671 . . 3  |-  ( ( W  e.  A  /\  C  e.  V )  ->  ( { <. ( E `  ndx ) ,  C >. } `  ( E `  ndx ) )  =  C )
4440, 43eqtrd 2457 . 2  |-  ( ( W  e.  A  /\  C  e.  V )  ->  ( ( ( W  |`  ( _V  \  {
( E `  ndx ) } ) )  u. 
{ <. ( E `  ndx ) ,  C >. } ) `  ( E `
 ndx ) )  =  C )
452, 9, 443eqtrrd 2462 1  |-  ( ( W  e.  A  /\  C  e.  V )  ->  C  =  ( E `
 ( W sSet  <. ( E `  ndx ) ,  C >. ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437    e. wcel 1872   _Vcvv 3017    \ cdif 3371    u. cun 3372    i^i cin 3373    C_ wss 3374   (/)c0 3699   {csn 3936   <.cop 3942    X. cxp 4789   dom cdm 4791    |` cres 4793   Rel wrel 4796   ` cfv 5539  (class class class)co 6244   ndxcnx 15056   sSet csts 15057  Slot cslot 15058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pr 4598  ax-un 6536
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-ral 2714  df-rex 2715  df-rab 2718  df-v 3019  df-sbc 3238  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-if 3850  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4158  df-br 4362  df-opab 4421  df-mpt 4422  df-id 4706  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-res 4803  df-iota 5503  df-fun 5541  df-fv 5547  df-ov 6247  df-oprab 6248  df-mpt2 6249  df-slot 15063  df-sets 15065
This theorem is referenced by:  ressbas  15117  oppchomfval  15557  oppccofval  15559  reschom  15673  oduleval  16315  oppgplusfval  16937  mgpplusg  17665  opprmulfval  17791  srasca  18342  sravsca  18343  sraip  18344  opsrle  18637  zlmsca  19029  zlmvsca  19030  znle  19044  thloc  19199  matmulr  19400  tuslem  21219  setsmstset  21429  tngds  21593  tngtset  21594  ttgval  24842  resvsca  28540  hlhilnvl  35433  uhgrepe  39281  cznrng  39548  cznnring  39549
  Copyright terms: Public domain W3C validator