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

Theorem setsid 17212
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 𝐸 = Slot (𝐸‘ndx)
Assertion
Ref Expression
setsid ((𝑊𝐴𝐶𝑉) → 𝐶 = (𝐸‘(𝑊 sSet ⟨(𝐸‘ndx), 𝐶⟩)))

Proof of Theorem setsid
StepHypRef Expression
1 setsval 17171 . . 3 ((𝑊𝐴𝐶𝑉) → (𝑊 sSet ⟨(𝐸‘ndx), 𝐶⟩) = ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}))
21fveq2d 6907 . 2 ((𝑊𝐴𝐶𝑉) → (𝐸‘(𝑊 sSet ⟨(𝐸‘ndx), 𝐶⟩)) = (𝐸‘((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩})))
3 setsid.e . . 3 𝐸 = Slot (𝐸‘ndx)
4 resexg 6038 . . . . 5 (𝑊𝐴 → (𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∈ V)
54adantr 479 . . . 4 ((𝑊𝐴𝐶𝑉) → (𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∈ V)
6 snex 5439 . . . 4 {⟨(𝐸‘ndx), 𝐶⟩} ∈ V
7 unexg 7759 . . . 4 (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∈ V ∧ {⟨(𝐸‘ndx), 𝐶⟩} ∈ V) → ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}) ∈ V)
85, 6, 7sylancl 584 . . 3 ((𝑊𝐴𝐶𝑉) → ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}) ∈ V)
93, 8strfvnd 17189 . 2 ((𝑊𝐴𝐶𝑉) → (𝐸‘((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩})) = (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩})‘(𝐸‘ndx)))
10 fvex 6916 . . . . . 6 (𝐸‘ndx) ∈ V
1110snid 4669 . . . . 5 (𝐸‘ndx) ∈ {(𝐸‘ndx)}
12 fvres 6922 . . . . 5 ((𝐸‘ndx) ∈ {(𝐸‘ndx)} → ((((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}) ↾ {(𝐸‘ndx)})‘(𝐸‘ndx)) = (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩})‘(𝐸‘ndx)))
1311, 12ax-mp 5 . . . 4 ((((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}) ↾ {(𝐸‘ndx)})‘(𝐸‘ndx)) = (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩})‘(𝐸‘ndx))
14 resres 6004 . . . . . . . . 9 ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) = (𝑊 ↾ ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)}))
15 disjdifr 4477 . . . . . . . . . . 11 ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)}) = ∅
1615reseq2i 5988 . . . . . . . . . 10 (𝑊 ↾ ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)})) = (𝑊 ↾ ∅)
17 res0 5995 . . . . . . . . . 10 (𝑊 ↾ ∅) = ∅
1816, 17eqtri 2754 . . . . . . . . 9 (𝑊 ↾ ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)})) = ∅
1914, 18eqtri 2754 . . . . . . . 8 ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) = ∅
2019a1i 11 . . . . . . 7 ((𝑊𝐴𝐶𝑉) → ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) = ∅)
21 elex 3482 . . . . . . . . . . 11 (𝐶𝑉𝐶 ∈ V)
2221adantl 480 . . . . . . . . . 10 ((𝑊𝐴𝐶𝑉) → 𝐶 ∈ V)
23 opelxpi 5721 . . . . . . . . . 10 (((𝐸‘ndx) ∈ V ∧ 𝐶 ∈ V) → ⟨(𝐸‘ndx), 𝐶⟩ ∈ (V × V))
2410, 22, 23sylancr 585 . . . . . . . . 9 ((𝑊𝐴𝐶𝑉) → ⟨(𝐸‘ndx), 𝐶⟩ ∈ (V × V))
25 opex 5472 . . . . . . . . . 10 ⟨(𝐸‘ndx), 𝐶⟩ ∈ V
2625relsn 5812 . . . . . . . . 9 (Rel {⟨(𝐸‘ndx), 𝐶⟩} ↔ ⟨(𝐸‘ndx), 𝐶⟩ ∈ (V × V))
2724, 26sylibr 233 . . . . . . . 8 ((𝑊𝐴𝐶𝑉) → Rel {⟨(𝐸‘ndx), 𝐶⟩})
28 dmsnopss 6227 . . . . . . . 8 dom {⟨(𝐸‘ndx), 𝐶⟩} ⊆ {(𝐸‘ndx)}
29 relssres 6033 . . . . . . . 8 ((Rel {⟨(𝐸‘ndx), 𝐶⟩} ∧ dom {⟨(𝐸‘ndx), 𝐶⟩} ⊆ {(𝐸‘ndx)}) → ({⟨(𝐸‘ndx), 𝐶⟩} ↾ {(𝐸‘ndx)}) = {⟨(𝐸‘ndx), 𝐶⟩})
3027, 28, 29sylancl 584 . . . . . . 7 ((𝑊𝐴𝐶𝑉) → ({⟨(𝐸‘ndx), 𝐶⟩} ↾ {(𝐸‘ndx)}) = {⟨(𝐸‘ndx), 𝐶⟩})
3120, 30uneq12d 4164 . . . . . 6 ((𝑊𝐴𝐶𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) ∪ ({⟨(𝐸‘ndx), 𝐶⟩} ↾ {(𝐸‘ndx)})) = (∅ ∪ {⟨(𝐸‘ndx), 𝐶⟩}))
32 resundir 6006 . . . . . 6 (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}) ↾ {(𝐸‘ndx)}) = (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) ∪ ({⟨(𝐸‘ndx), 𝐶⟩} ↾ {(𝐸‘ndx)}))
33 un0 4395 . . . . . . 7 ({⟨(𝐸‘ndx), 𝐶⟩} ∪ ∅) = {⟨(𝐸‘ndx), 𝐶⟩}
34 uncom 4153 . . . . . . 7 ({⟨(𝐸‘ndx), 𝐶⟩} ∪ ∅) = (∅ ∪ {⟨(𝐸‘ndx), 𝐶⟩})
3533, 34eqtr3i 2756 . . . . . 6 {⟨(𝐸‘ndx), 𝐶⟩} = (∅ ∪ {⟨(𝐸‘ndx), 𝐶⟩})
3631, 32, 353eqtr4g 2791 . . . . 5 ((𝑊𝐴𝐶𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}) ↾ {(𝐸‘ndx)}) = {⟨(𝐸‘ndx), 𝐶⟩})
3736fveq1d 6905 . . . 4 ((𝑊𝐴𝐶𝑉) → ((((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}) ↾ {(𝐸‘ndx)})‘(𝐸‘ndx)) = ({⟨(𝐸‘ndx), 𝐶⟩}‘(𝐸‘ndx)))
3813, 37eqtr3id 2780 . . 3 ((𝑊𝐴𝐶𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩})‘(𝐸‘ndx)) = ({⟨(𝐸‘ndx), 𝐶⟩}‘(𝐸‘ndx)))
3910a1i 11 . . . 4 ((𝑊𝐴𝐶𝑉) → (𝐸‘ndx) ∈ V)
40 fvsng 7196 . . . 4 (((𝐸‘ndx) ∈ V ∧ 𝐶𝑉) → ({⟨(𝐸‘ndx), 𝐶⟩}‘(𝐸‘ndx)) = 𝐶)
4139, 40sylancom 586 . . 3 ((𝑊𝐴𝐶𝑉) → ({⟨(𝐸‘ndx), 𝐶⟩}‘(𝐸‘ndx)) = 𝐶)
4238, 41eqtrd 2766 . 2 ((𝑊𝐴𝐶𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩})‘(𝐸‘ndx)) = 𝐶)
432, 9, 423eqtrrd 2771 1 ((𝑊𝐴𝐶𝑉) → 𝐶 = (𝐸‘(𝑊 sSet ⟨(𝐸‘ndx), 𝐶⟩)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394   = wceq 1534  wcel 2099  Vcvv 3462  cdif 3944  cun 3945  cin 3946  wss 3947  c0 4325  {csn 4633  cop 4639   × cxp 5682  dom cdm 5684  cres 5686  Rel wrel 5689  cfv 6556  (class class class)co 7426   sSet csts 17167  Slot cslot 17185  ndxcnx 17197
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5306  ax-nul 5313  ax-pr 5435  ax-un 7748
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4916  df-br 5156  df-opab 5218  df-mpt 5239  df-id 5582  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-res 5696  df-iota 6508  df-fun 6558  df-fv 6564  df-ov 7429  df-oprab 7430  df-mpo 7431  df-sets 17168  df-slot 17186
This theorem is referenced by:  ressbas  17250  ressbasOLD  17251  oppchomfval  17729  oppchomfvalOLD  17730  oppccofval  17732  reschom  17849  oduleval  18316  oppgplusfval  19344  mgpplusg  20123  opprmulfval  20320  rmodislmod  20908  rmodislmodOLD  20909  srasca  21164  srascaOLD  21165  sravsca  21166  sravscaOLD  21167  sraip  21168  zlmsca  21516  zlmvsca  21517  znle  21532  thloc  21699  opsrle  22056  matmulr  22434  tuslem  24265  tuslemOLD  24266  setsmstset  24479  tngds  24658  tngdsOLD  24659  tngtset  24660  ttgval  28805  ttgvalOLD  28806  setsiedg  28975  resvsca  33206  hlhilnvl  41655  mnringmulrd  43913  cznrng  47656  cznnring  47657  prstchomval  48413  prstcthin  48415
  Copyright terms: Public domain W3C validator