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

Theorem setsid 16372
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 16347 . . 3 ((𝑊𝐴𝐶𝑉) → (𝑊 sSet ⟨(𝐸‘ndx), 𝐶⟩) = ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}))
21fveq2d 6547 . 2 ((𝑊𝐴𝐶𝑉) → (𝐸‘(𝑊 sSet ⟨(𝐸‘ndx), 𝐶⟩)) = (𝐸‘((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩})))
3 setsid.e . . 3 𝐸 = Slot (𝐸‘ndx)
4 resexg 5784 . . . . 5 (𝑊𝐴 → (𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∈ V)
54adantr 481 . . . 4 ((𝑊𝐴𝐶𝑉) → (𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∈ V)
6 snex 5228 . . . 4 {⟨(𝐸‘ndx), 𝐶⟩} ∈ V
7 unexg 7334 . . . 4 (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∈ V ∧ {⟨(𝐸‘ndx), 𝐶⟩} ∈ V) → ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}) ∈ V)
85, 6, 7sylancl 586 . . 3 ((𝑊𝐴𝐶𝑉) → ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}) ∈ V)
93, 8strfvnd 16336 . 2 ((𝑊𝐴𝐶𝑉) → (𝐸‘((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩})) = (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩})‘(𝐸‘ndx)))
10 fvex 6556 . . . . . 6 (𝐸‘ndx) ∈ V
1110snid 4510 . . . . 5 (𝐸‘ndx) ∈ {(𝐸‘ndx)}
12 fvres 6562 . . . . 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 5752 . . . . . . . . 9 ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) = (𝑊 ↾ ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)}))
15 incom 4103 . . . . . . . . . . . 12 ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)}) = ({(𝐸‘ndx)} ∩ (V ∖ {(𝐸‘ndx)}))
16 disjdif 4339 . . . . . . . . . . . 12 ({(𝐸‘ndx)} ∩ (V ∖ {(𝐸‘ndx)})) = ∅
1715, 16eqtri 2819 . . . . . . . . . . 11 ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)}) = ∅
1817reseq2i 5736 . . . . . . . . . 10 (𝑊 ↾ ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)})) = (𝑊 ↾ ∅)
19 res0 5743 . . . . . . . . . 10 (𝑊 ↾ ∅) = ∅
2018, 19eqtri 2819 . . . . . . . . 9 (𝑊 ↾ ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)})) = ∅
2114, 20eqtri 2819 . . . . . . . 8 ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) = ∅
2221a1i 11 . . . . . . 7 ((𝑊𝐴𝐶𝑉) → ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) = ∅)
23 elex 3455 . . . . . . . . . . 11 (𝐶𝑉𝐶 ∈ V)
2423adantl 482 . . . . . . . . . 10 ((𝑊𝐴𝐶𝑉) → 𝐶 ∈ V)
25 opelxpi 5485 . . . . . . . . . 10 (((𝐸‘ndx) ∈ V ∧ 𝐶 ∈ V) → ⟨(𝐸‘ndx), 𝐶⟩ ∈ (V × V))
2610, 24, 25sylancr 587 . . . . . . . . 9 ((𝑊𝐴𝐶𝑉) → ⟨(𝐸‘ndx), 𝐶⟩ ∈ (V × V))
27 opex 5253 . . . . . . . . . 10 ⟨(𝐸‘ndx), 𝐶⟩ ∈ V
2827relsn 5568 . . . . . . . . 9 (Rel {⟨(𝐸‘ndx), 𝐶⟩} ↔ ⟨(𝐸‘ndx), 𝐶⟩ ∈ (V × V))
2926, 28sylibr 235 . . . . . . . 8 ((𝑊𝐴𝐶𝑉) → Rel {⟨(𝐸‘ndx), 𝐶⟩})
30 dmsnopss 5951 . . . . . . . 8 dom {⟨(𝐸‘ndx), 𝐶⟩} ⊆ {(𝐸‘ndx)}
31 relssres 5779 . . . . . . . 8 ((Rel {⟨(𝐸‘ndx), 𝐶⟩} ∧ dom {⟨(𝐸‘ndx), 𝐶⟩} ⊆ {(𝐸‘ndx)}) → ({⟨(𝐸‘ndx), 𝐶⟩} ↾ {(𝐸‘ndx)}) = {⟨(𝐸‘ndx), 𝐶⟩})
3229, 30, 31sylancl 586 . . . . . . 7 ((𝑊𝐴𝐶𝑉) → ({⟨(𝐸‘ndx), 𝐶⟩} ↾ {(𝐸‘ndx)}) = {⟨(𝐸‘ndx), 𝐶⟩})
3322, 32uneq12d 4065 . . . . . 6 ((𝑊𝐴𝐶𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) ∪ ({⟨(𝐸‘ndx), 𝐶⟩} ↾ {(𝐸‘ndx)})) = (∅ ∪ {⟨(𝐸‘ndx), 𝐶⟩}))
34 resundir 5754 . . . . . 6 (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}) ↾ {(𝐸‘ndx)}) = (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) ∪ ({⟨(𝐸‘ndx), 𝐶⟩} ↾ {(𝐸‘ndx)}))
35 un0 4268 . . . . . . 7 ({⟨(𝐸‘ndx), 𝐶⟩} ∪ ∅) = {⟨(𝐸‘ndx), 𝐶⟩}
36 uncom 4054 . . . . . . 7 ({⟨(𝐸‘ndx), 𝐶⟩} ∪ ∅) = (∅ ∪ {⟨(𝐸‘ndx), 𝐶⟩})
3735, 36eqtr3i 2821 . . . . . 6 {⟨(𝐸‘ndx), 𝐶⟩} = (∅ ∪ {⟨(𝐸‘ndx), 𝐶⟩})
3833, 34, 373eqtr4g 2856 . . . . 5 ((𝑊𝐴𝐶𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}) ↾ {(𝐸‘ndx)}) = {⟨(𝐸‘ndx), 𝐶⟩})
3938fveq1d 6545 . . . 4 ((𝑊𝐴𝐶𝑉) → ((((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}) ↾ {(𝐸‘ndx)})‘(𝐸‘ndx)) = ({⟨(𝐸‘ndx), 𝐶⟩}‘(𝐸‘ndx)))
4013, 39syl5eqr 2845 . . 3 ((𝑊𝐴𝐶𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩})‘(𝐸‘ndx)) = ({⟨(𝐸‘ndx), 𝐶⟩}‘(𝐸‘ndx)))
4110a1i 11 . . . 4 ((𝑊𝐴𝐶𝑉) → (𝐸‘ndx) ∈ V)
42 fvsng 6810 . . . 4 (((𝐸‘ndx) ∈ V ∧ 𝐶𝑉) → ({⟨(𝐸‘ndx), 𝐶⟩}‘(𝐸‘ndx)) = 𝐶)
4341, 42sylancom 588 . . 3 ((𝑊𝐴𝐶𝑉) → ({⟨(𝐸‘ndx), 𝐶⟩}‘(𝐸‘ndx)) = 𝐶)
4440, 43eqtrd 2831 . 2 ((𝑊𝐴𝐶𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩})‘(𝐸‘ndx)) = 𝐶)
452, 9, 443eqtrrd 2836 1 ((𝑊𝐴𝐶𝑉) → 𝐶 = (𝐸‘(𝑊 sSet ⟨(𝐸‘ndx), 𝐶⟩)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1522  wcel 2081  Vcvv 3437  cdif 3860  cun 3861  cin 3862  wss 3863  c0 4215  {csn 4476  cop 4482   × cxp 5446  dom cdm 5448  cres 5450  Rel wrel 5453  cfv 6230  (class class class)co 7021  ndxcnx 16314   sSet csts 16315  Slot cslot 16316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5099  ax-nul 5106  ax-pr 5226  ax-un 7324
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3710  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-nul 4216  df-if 4386  df-sn 4477  df-pr 4479  df-op 4483  df-uni 4750  df-br 4967  df-opab 5029  df-mpt 5046  df-id 5353  df-xp 5454  df-rel 5455  df-cnv 5456  df-co 5457  df-dm 5458  df-res 5460  df-iota 6194  df-fun 6232  df-fv 6238  df-ov 7024  df-oprab 7025  df-mpo 7026  df-slot 16321  df-sets 16324
This theorem is referenced by:  ressbas  16388  oppchomfval  16818  oppccofval  16820  reschom  16934  oduleval  17575  oppgplusfval  18222  mgpplusg  18938  opprmulfval  19070  rmodislmod  19397  srasca  19648  sravsca  19649  sraip  19650  opsrle  19948  zlmsca  20355  zlmvsca  20356  znle  20370  thloc  20530  matmulr  20736  tuslem  22564  setsmstset  22775  tngds  22945  tngtset  22946  ttgval  26349  setsiedg  26509  resvsca  30562  hlhilnvl  38642  cznrng  43730  cznnring  43731
  Copyright terms: Public domain W3C validator