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

Theorem setsnid 16385
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.)
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 16348 . . 3 (𝑊 ∈ V → (𝐸𝑊) = (𝑊‘(𝐸‘ndx)))
4 ovex 7002 . . . . 5 (𝑊 sSet ⟨𝐷, 𝐶⟩) ∈ V
54, 1strfvn 16351 . . . 4 (𝐸‘(𝑊 sSet ⟨𝐷, 𝐶⟩)) = ((𝑊 sSet ⟨𝐷, 𝐶⟩)‘(𝐸‘ndx))
6 setsres 16371 . . . . . 6 (𝑊 ∈ V → ((𝑊 sSet ⟨𝐷, 𝐶⟩) ↾ (V ∖ {𝐷})) = (𝑊 ↾ (V ∖ {𝐷})))
76fveq1d 6495 . . . . 5 (𝑊 ∈ V → (((𝑊 sSet ⟨𝐷, 𝐶⟩) ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = ((𝑊 ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)))
8 fvex 6506 . . . . . . 7 (𝐸‘ndx) ∈ V
9 setsnid.n . . . . . . 7 (𝐸‘ndx) ≠ 𝐷
10 eldifsn 4587 . . . . . . 7 ((𝐸‘ndx) ∈ (V ∖ {𝐷}) ↔ ((𝐸‘ndx) ∈ V ∧ (𝐸‘ndx) ≠ 𝐷))
118, 9, 10mpbir2an 698 . . . . . 6 (𝐸‘ndx) ∈ (V ∖ {𝐷})
12 fvres 6512 . . . . . 6 ((𝐸‘ndx) ∈ (V ∖ {𝐷}) → (((𝑊 sSet ⟨𝐷, 𝐶⟩) ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = ((𝑊 sSet ⟨𝐷, 𝐶⟩)‘(𝐸‘ndx)))
1311, 12ax-mp 5 . . . . 5 (((𝑊 sSet ⟨𝐷, 𝐶⟩) ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = ((𝑊 sSet ⟨𝐷, 𝐶⟩)‘(𝐸‘ndx))
14 fvres 6512 . . . . . 6 ((𝐸‘ndx) ∈ (V ∖ {𝐷}) → ((𝑊 ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = (𝑊‘(𝐸‘ndx)))
1511, 14ax-mp 5 . . . . 5 ((𝑊 ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = (𝑊‘(𝐸‘ndx))
167, 13, 153eqtr3g 2831 . . . 4 (𝑊 ∈ V → ((𝑊 sSet ⟨𝐷, 𝐶⟩)‘(𝐸‘ndx)) = (𝑊‘(𝐸‘ndx)))
175, 16syl5eq 2820 . . 3 (𝑊 ∈ V → (𝐸‘(𝑊 sSet ⟨𝐷, 𝐶⟩)) = (𝑊‘(𝐸‘ndx)))
183, 17eqtr4d 2811 . 2 (𝑊 ∈ V → (𝐸𝑊) = (𝐸‘(𝑊 sSet ⟨𝐷, 𝐶⟩)))
191str0 16381 . . 3 ∅ = (𝐸‘∅)
20 fvprc 6486 . . 3 𝑊 ∈ V → (𝐸𝑊) = ∅)
21 reldmsets 16357 . . . . 5 Rel dom sSet
2221ovprc1 7008 . . . 4 𝑊 ∈ V → (𝑊 sSet ⟨𝐷, 𝐶⟩) = ∅)
2322fveq2d 6497 . . 3 𝑊 ∈ V → (𝐸‘(𝑊 sSet ⟨𝐷, 𝐶⟩)) = (𝐸‘∅))
2419, 20, 233eqtr4a 2834 . 2 𝑊 ∈ V → (𝐸𝑊) = (𝐸‘(𝑊 sSet ⟨𝐷, 𝐶⟩)))
2518, 24pm2.61i 177 1 (𝐸𝑊) = (𝐸‘(𝑊 sSet ⟨𝐷, 𝐶⟩))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1507  wcel 2048  wne 2961  Vcvv 3409  cdif 3822  c0 4173  {csn 4435  cop 4441  cres 5402  cfv 6182  (class class class)co 6970  ndxcnx 16326   sSet csts 16327  Slot cslot 16328
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2745  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-ral 3087  df-rex 3088  df-rab 3091  df-v 3411  df-sbc 3678  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-nul 4174  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4707  df-br 4924  df-opab 4986  df-mpt 5003  df-id 5305  df-xp 5406  df-rel 5407  df-cnv 5408  df-co 5409  df-dm 5410  df-res 5412  df-iota 6146  df-fun 6184  df-fv 6190  df-ov 6973  df-oprab 6974  df-mpo 6975  df-slot 16333  df-sets 16336
This theorem is referenced by:  resslem  16403  oppchomfval  16832  oppcbas  16836  rescbas  16947  rescco  16950  rescabs  16951  odubas  17591  oppglem  18239  mgplem  18957  opprlem  19091  rmodislmod  19414  sralem  19661  srasca  19665  sravsca  19666  opsrbaslem  19961  zlmlem  20356  zlmsca  20360  znbaslem  20377  thlbas  20532  thlle  20533  matbas  20716  matplusg  20717  matsca  20718  matvsca  20719  tuslem  22569  setsmsbas  22778  setsmsds  22779  tnglem  22942  tngds  22950  ttgval  26354  ttglem  26355  cchhllem  26366  setsvtx  26513  resvlem  30539  zlmds  30806  zlmtset  30807  hlhilslem  38467  cznrnglem  43528  cznabel  43529  cznrng  43530
  Copyright terms: Public domain W3C validator