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

Theorem setsid 16530
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 16505 . . 3 ((𝑊𝐴𝐶𝑉) → (𝑊 sSet ⟨(𝐸‘ndx), 𝐶⟩) = ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}))
21fveq2d 6649 . 2 ((𝑊𝐴𝐶𝑉) → (𝐸‘(𝑊 sSet ⟨(𝐸‘ndx), 𝐶⟩)) = (𝐸‘((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩})))
3 setsid.e . . 3 𝐸 = Slot (𝐸‘ndx)
4 resexg 5864 . . . . 5 (𝑊𝐴 → (𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∈ V)
54adantr 484 . . . 4 ((𝑊𝐴𝐶𝑉) → (𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∈ V)
6 snex 5297 . . . 4 {⟨(𝐸‘ndx), 𝐶⟩} ∈ V
7 unexg 7452 . . . 4 (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∈ V ∧ {⟨(𝐸‘ndx), 𝐶⟩} ∈ V) → ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}) ∈ V)
85, 6, 7sylancl 589 . . 3 ((𝑊𝐴𝐶𝑉) → ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}) ∈ V)
93, 8strfvnd 16494 . 2 ((𝑊𝐴𝐶𝑉) → (𝐸‘((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩})) = (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩})‘(𝐸‘ndx)))
10 fvex 6658 . . . . . 6 (𝐸‘ndx) ∈ V
1110snid 4561 . . . . 5 (𝐸‘ndx) ∈ {(𝐸‘ndx)}
12 fvres 6664 . . . . 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 5831 . . . . . . . . 9 ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) = (𝑊 ↾ ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)}))
15 incom 4128 . . . . . . . . . . . 12 ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)}) = ({(𝐸‘ndx)} ∩ (V ∖ {(𝐸‘ndx)}))
16 disjdif 4379 . . . . . . . . . . . 12 ({(𝐸‘ndx)} ∩ (V ∖ {(𝐸‘ndx)})) = ∅
1715, 16eqtri 2821 . . . . . . . . . . 11 ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)}) = ∅
1817reseq2i 5815 . . . . . . . . . 10 (𝑊 ↾ ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)})) = (𝑊 ↾ ∅)
19 res0 5822 . . . . . . . . . 10 (𝑊 ↾ ∅) = ∅
2018, 19eqtri 2821 . . . . . . . . 9 (𝑊 ↾ ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)})) = ∅
2114, 20eqtri 2821 . . . . . . . 8 ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) = ∅
2221a1i 11 . . . . . . 7 ((𝑊𝐴𝐶𝑉) → ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) = ∅)
23 elex 3459 . . . . . . . . . . 11 (𝐶𝑉𝐶 ∈ V)
2423adantl 485 . . . . . . . . . 10 ((𝑊𝐴𝐶𝑉) → 𝐶 ∈ V)
25 opelxpi 5556 . . . . . . . . . 10 (((𝐸‘ndx) ∈ V ∧ 𝐶 ∈ V) → ⟨(𝐸‘ndx), 𝐶⟩ ∈ (V × V))
2610, 24, 25sylancr 590 . . . . . . . . 9 ((𝑊𝐴𝐶𝑉) → ⟨(𝐸‘ndx), 𝐶⟩ ∈ (V × V))
27 opex 5321 . . . . . . . . . 10 ⟨(𝐸‘ndx), 𝐶⟩ ∈ V
2827relsn 5641 . . . . . . . . 9 (Rel {⟨(𝐸‘ndx), 𝐶⟩} ↔ ⟨(𝐸‘ndx), 𝐶⟩ ∈ (V × V))
2926, 28sylibr 237 . . . . . . . 8 ((𝑊𝐴𝐶𝑉) → Rel {⟨(𝐸‘ndx), 𝐶⟩})
30 dmsnopss 6038 . . . . . . . 8 dom {⟨(𝐸‘ndx), 𝐶⟩} ⊆ {(𝐸‘ndx)}
31 relssres 5859 . . . . . . . 8 ((Rel {⟨(𝐸‘ndx), 𝐶⟩} ∧ dom {⟨(𝐸‘ndx), 𝐶⟩} ⊆ {(𝐸‘ndx)}) → ({⟨(𝐸‘ndx), 𝐶⟩} ↾ {(𝐸‘ndx)}) = {⟨(𝐸‘ndx), 𝐶⟩})
3229, 30, 31sylancl 589 . . . . . . 7 ((𝑊𝐴𝐶𝑉) → ({⟨(𝐸‘ndx), 𝐶⟩} ↾ {(𝐸‘ndx)}) = {⟨(𝐸‘ndx), 𝐶⟩})
3322, 32uneq12d 4091 . . . . . 6 ((𝑊𝐴𝐶𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) ∪ ({⟨(𝐸‘ndx), 𝐶⟩} ↾ {(𝐸‘ndx)})) = (∅ ∪ {⟨(𝐸‘ndx), 𝐶⟩}))
34 resundir 5833 . . . . . 6 (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}) ↾ {(𝐸‘ndx)}) = (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) ∪ ({⟨(𝐸‘ndx), 𝐶⟩} ↾ {(𝐸‘ndx)}))
35 un0 4298 . . . . . . 7 ({⟨(𝐸‘ndx), 𝐶⟩} ∪ ∅) = {⟨(𝐸‘ndx), 𝐶⟩}
36 uncom 4080 . . . . . . 7 ({⟨(𝐸‘ndx), 𝐶⟩} ∪ ∅) = (∅ ∪ {⟨(𝐸‘ndx), 𝐶⟩})
3735, 36eqtr3i 2823 . . . . . 6 {⟨(𝐸‘ndx), 𝐶⟩} = (∅ ∪ {⟨(𝐸‘ndx), 𝐶⟩})
3833, 34, 373eqtr4g 2858 . . . . 5 ((𝑊𝐴𝐶𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}) ↾ {(𝐸‘ndx)}) = {⟨(𝐸‘ndx), 𝐶⟩})
3938fveq1d 6647 . . . 4 ((𝑊𝐴𝐶𝑉) → ((((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}) ↾ {(𝐸‘ndx)})‘(𝐸‘ndx)) = ({⟨(𝐸‘ndx), 𝐶⟩}‘(𝐸‘ndx)))
4013, 39syl5eqr 2847 . . 3 ((𝑊𝐴𝐶𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩})‘(𝐸‘ndx)) = ({⟨(𝐸‘ndx), 𝐶⟩}‘(𝐸‘ndx)))
4110a1i 11 . . . 4 ((𝑊𝐴𝐶𝑉) → (𝐸‘ndx) ∈ V)
42 fvsng 6919 . . . 4 (((𝐸‘ndx) ∈ V ∧ 𝐶𝑉) → ({⟨(𝐸‘ndx), 𝐶⟩}‘(𝐸‘ndx)) = 𝐶)
4341, 42sylancom 591 . . 3 ((𝑊𝐴𝐶𝑉) → ({⟨(𝐸‘ndx), 𝐶⟩}‘(𝐸‘ndx)) = 𝐶)
4440, 43eqtrd 2833 . 2 ((𝑊𝐴𝐶𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩})‘(𝐸‘ndx)) = 𝐶)
452, 9, 443eqtrrd 2838 1 ((𝑊𝐴𝐶𝑉) → 𝐶 = (𝐸‘(𝑊 sSet ⟨(𝐸‘ndx), 𝐶⟩)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  wcel 2111  Vcvv 3441  cdif 3878  cun 3879  cin 3880  wss 3881  c0 4243  {csn 4525  cop 4531   × cxp 5517  dom cdm 5519  cres 5521  Rel wrel 5524  cfv 6324  (class class class)co 7135  ndxcnx 16472   sSet csts 16473  Slot cslot 16474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295  ax-un 7441
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-res 5531  df-iota 6283  df-fun 6326  df-fv 6332  df-ov 7138  df-oprab 7139  df-mpo 7140  df-slot 16479  df-sets 16482
This theorem is referenced by:  ressbas  16546  oppchomfval  16976  oppccofval  16978  reschom  17092  oduleval  17733  oppgplusfval  18468  mgpplusg  19236  opprmulfval  19371  rmodislmod  19695  srasca  19946  sravsca  19947  sraip  19948  zlmsca  20214  zlmvsca  20215  znle  20228  thloc  20388  opsrle  20715  matmulr  21043  tuslem  22873  setsmstset  23084  tngds  23254  tngtset  23255  ttgval  26669  setsiedg  26829  resvsca  30954  hlhilnvl  39246  mnringmulrd  40929  cznrng  44577  cznnring  44578
  Copyright terms: Public domain W3C validator