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

Theorem setsnid 17243
Description: Value of the structure replacement function at an untouched index. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) (Proof shortened by AV, 7-Nov-2024.)
Hypotheses
Ref Expression
setsid.e 𝐸 = Slot (𝐸‘ndx)
setsnid.n (𝐸‘ndx) ≠ 𝐷
Assertion
Ref Expression
setsnid (𝐸𝑊) = (𝐸‘(𝑊 sSet ⟨𝐷, 𝐶⟩))

Proof of Theorem setsnid
StepHypRef Expression
1 setsid.e . . . 4 𝐸 = Slot (𝐸‘ndx)
2 id 22 . . . 4 (𝑊 ∈ V → 𝑊 ∈ V)
31, 2strfvnd 17219 . . 3 (𝑊 ∈ V → (𝐸𝑊) = (𝑊‘(𝐸‘ndx)))
4 ovex 7464 . . . . 5 (𝑊 sSet ⟨𝐷, 𝐶⟩) ∈ V
54, 1strfvn 17220 . . . 4 (𝐸‘(𝑊 sSet ⟨𝐷, 𝐶⟩)) = ((𝑊 sSet ⟨𝐷, 𝐶⟩)‘(𝐸‘ndx))
6 setsres 17212 . . . . . 6 (𝑊 ∈ V → ((𝑊 sSet ⟨𝐷, 𝐶⟩) ↾ (V ∖ {𝐷})) = (𝑊 ↾ (V ∖ {𝐷})))
76fveq1d 6909 . . . . 5 (𝑊 ∈ V → (((𝑊 sSet ⟨𝐷, 𝐶⟩) ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = ((𝑊 ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)))
8 fvex 6920 . . . . . . 7 (𝐸‘ndx) ∈ V
9 setsnid.n . . . . . . 7 (𝐸‘ndx) ≠ 𝐷
10 eldifsn 4791 . . . . . . 7 ((𝐸‘ndx) ∈ (V ∖ {𝐷}) ↔ ((𝐸‘ndx) ∈ V ∧ (𝐸‘ndx) ≠ 𝐷))
118, 9, 10mpbir2an 711 . . . . . 6 (𝐸‘ndx) ∈ (V ∖ {𝐷})
12 fvres 6926 . . . . . 6 ((𝐸‘ndx) ∈ (V ∖ {𝐷}) → (((𝑊 sSet ⟨𝐷, 𝐶⟩) ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = ((𝑊 sSet ⟨𝐷, 𝐶⟩)‘(𝐸‘ndx)))
1311, 12ax-mp 5 . . . . 5 (((𝑊 sSet ⟨𝐷, 𝐶⟩) ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = ((𝑊 sSet ⟨𝐷, 𝐶⟩)‘(𝐸‘ndx))
14 fvres 6926 . . . . . 6 ((𝐸‘ndx) ∈ (V ∖ {𝐷}) → ((𝑊 ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = (𝑊‘(𝐸‘ndx)))
1511, 14ax-mp 5 . . . . 5 ((𝑊 ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = (𝑊‘(𝐸‘ndx))
167, 13, 153eqtr3g 2798 . . . 4 (𝑊 ∈ V → ((𝑊 sSet ⟨𝐷, 𝐶⟩)‘(𝐸‘ndx)) = (𝑊‘(𝐸‘ndx)))
175, 16eqtrid 2787 . . 3 (𝑊 ∈ V → (𝐸‘(𝑊 sSet ⟨𝐷, 𝐶⟩)) = (𝑊‘(𝐸‘ndx)))
183, 17eqtr4d 2778 . 2 (𝑊 ∈ V → (𝐸𝑊) = (𝐸‘(𝑊 sSet ⟨𝐷, 𝐶⟩)))
191str0 17223 . . . 4 ∅ = (𝐸‘∅)
2019eqcomi 2744 . . 3 (𝐸‘∅) = ∅
21 eqid 2735 . . 3 (𝑊 sSet ⟨𝐷, 𝐶⟩) = (𝑊 sSet ⟨𝐷, 𝐶⟩)
22 reldmsets 17199 . . 3 Rel dom sSet
2320, 21, 22oveqprc 17226 . 2 𝑊 ∈ V → (𝐸𝑊) = (𝐸‘(𝑊 sSet ⟨𝐷, 𝐶⟩)))
2418, 23pm2.61i 182 1 (𝐸𝑊) = (𝐸‘(𝑊 sSet ⟨𝐷, 𝐶⟩))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1537  wcel 2106  wne 2938  Vcvv 3478  cdif 3960  c0 4339  {csn 4631  cop 4637  cres 5691  cfv 6563  (class class class)co 7431   sSet csts 17197  Slot cslot 17215  ndxcnx 17227
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-sbc 3792  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-res 5701  df-iota 6516  df-fun 6565  df-fv 6571  df-ov 7434  df-oprab 7435  df-mpo 7436  df-sets 17198  df-slot 17216
This theorem is referenced by:  resseqnbas  17287  resslemOLD  17288  oppchomfval  17759  oppchomfvalOLD  17760  oppcbas  17764  oppcbasOLD  17765  rescbas  17877  rescbasOLD  17878  rescco  17881  resccoOLD  17882  rescabs  17883  rescabsOLD  17884  odubas  18348  odubasOLD  18349  setsplusg  19381  oppglemOLD  19382  mgplemOLD  20157  opprlem  20356  opprlemOLD  20357  rmodislmod  20945  rmodislmodOLD  20946  sralem  21193  sralemOLD  21194  srasca  21201  srascaOLD  21202  sravsca  21203  sravscaOLD  21204  zlmlem  21545  zlmlemOLD  21546  zlmsca  21553  znbaslem  21571  znbaslemOLD  21572  thlbas  21732  thlbasOLD  21733  thlle  21734  thlleOLD  21735  opsrbaslem  22085  opsrbaslemOLD  22086  matbas  22433  matplusg  22434  matsca  22435  matscaOLD  22436  matvsca  22437  matvscaOLD  22438  tuslem  24291  tuslemOLD  24292  setsmsbas  24501  setsmsbasOLD  24502  setsmsds  24503  setsmsdsOLD  24504  tnglem  24669  tnglemOLD  24670  tngds  24684  tngdsOLD  24685  ttgval  28898  ttgvalOLD  28899  ttglem  28900  ttglemOLD  28901  cchhllem  28916  cchhllemOLD  28917  setsvtx  29067  resvlem  33337  resvlemOLD  33338  zlmds  33923  zlmdsOLD  33924  zlmtset  33925  zlmtsetOLD  33926  hlhilslem  41921  hlhilslemOLD  41922  mnringnmulrd  44205  mnringnmulrdOLD  44206  cznrnglem  48103  cznabel  48104  cznrng  48105  prstcnidlem  48866  prstcnid  48867
  Copyright terms: Public domain W3C validator