# Metamath Proof Explorer

## Theorem setsnid

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)

Ref Expression
Hypotheses setsid.e ${⊢}{E}=\mathrm{Slot}{E}\left(\mathrm{ndx}\right)$
setsnid.n ${⊢}{E}\left(\mathrm{ndx}\right)\ne {D}$
Assertion setsnid ${⊢}{E}\left({W}\right)={E}\left({W}\mathrm{sSet}⟨{D},{C}⟩\right)$

### Proof

Step Hyp Ref Expression
1 setsid.e ${⊢}{E}=\mathrm{Slot}{E}\left(\mathrm{ndx}\right)$
2 setsnid.n ${⊢}{E}\left(\mathrm{ndx}\right)\ne {D}$
3 id ${⊢}{W}\in \mathrm{V}\to {W}\in \mathrm{V}$
4 1 3 strfvnd ${⊢}{W}\in \mathrm{V}\to {E}\left({W}\right)={W}\left({E}\left(\mathrm{ndx}\right)\right)$
5 ovex ${⊢}{W}\mathrm{sSet}⟨{D},{C}⟩\in \mathrm{V}$
6 5 1 strfvn ${⊢}{E}\left({W}\mathrm{sSet}⟨{D},{C}⟩\right)=\left({W}\mathrm{sSet}⟨{D},{C}⟩\right)\left({E}\left(\mathrm{ndx}\right)\right)$
7 setsres ${⊢}{W}\in \mathrm{V}\to {\left({W}\mathrm{sSet}⟨{D},{C}⟩\right)↾}_{\left(\mathrm{V}\setminus \left\{{D}\right\}\right)}={{W}↾}_{\left(\mathrm{V}\setminus \left\{{D}\right\}\right)}$
8 7 fveq1d ${⊢}{W}\in \mathrm{V}\to \left({\left({W}\mathrm{sSet}⟨{D},{C}⟩\right)↾}_{\left(\mathrm{V}\setminus \left\{{D}\right\}\right)}\right)\left({E}\left(\mathrm{ndx}\right)\right)=\left({{W}↾}_{\left(\mathrm{V}\setminus \left\{{D}\right\}\right)}\right)\left({E}\left(\mathrm{ndx}\right)\right)$
9 fvex ${⊢}{E}\left(\mathrm{ndx}\right)\in \mathrm{V}$
10 eldifsn ${⊢}{E}\left(\mathrm{ndx}\right)\in \left(\mathrm{V}\setminus \left\{{D}\right\}\right)↔\left({E}\left(\mathrm{ndx}\right)\in \mathrm{V}\wedge {E}\left(\mathrm{ndx}\right)\ne {D}\right)$
11 9 2 10 mpbir2an ${⊢}{E}\left(\mathrm{ndx}\right)\in \left(\mathrm{V}\setminus \left\{{D}\right\}\right)$
12 fvres ${⊢}{E}\left(\mathrm{ndx}\right)\in \left(\mathrm{V}\setminus \left\{{D}\right\}\right)\to \left({\left({W}\mathrm{sSet}⟨{D},{C}⟩\right)↾}_{\left(\mathrm{V}\setminus \left\{{D}\right\}\right)}\right)\left({E}\left(\mathrm{ndx}\right)\right)=\left({W}\mathrm{sSet}⟨{D},{C}⟩\right)\left({E}\left(\mathrm{ndx}\right)\right)$
13 11 12 ax-mp ${⊢}\left({\left({W}\mathrm{sSet}⟨{D},{C}⟩\right)↾}_{\left(\mathrm{V}\setminus \left\{{D}\right\}\right)}\right)\left({E}\left(\mathrm{ndx}\right)\right)=\left({W}\mathrm{sSet}⟨{D},{C}⟩\right)\left({E}\left(\mathrm{ndx}\right)\right)$
14 fvres ${⊢}{E}\left(\mathrm{ndx}\right)\in \left(\mathrm{V}\setminus \left\{{D}\right\}\right)\to \left({{W}↾}_{\left(\mathrm{V}\setminus \left\{{D}\right\}\right)}\right)\left({E}\left(\mathrm{ndx}\right)\right)={W}\left({E}\left(\mathrm{ndx}\right)\right)$
15 11 14 ax-mp ${⊢}\left({{W}↾}_{\left(\mathrm{V}\setminus \left\{{D}\right\}\right)}\right)\left({E}\left(\mathrm{ndx}\right)\right)={W}\left({E}\left(\mathrm{ndx}\right)\right)$
16 8 13 15 3eqtr3g ${⊢}{W}\in \mathrm{V}\to \left({W}\mathrm{sSet}⟨{D},{C}⟩\right)\left({E}\left(\mathrm{ndx}\right)\right)={W}\left({E}\left(\mathrm{ndx}\right)\right)$
17 6 16 syl5eq ${⊢}{W}\in \mathrm{V}\to {E}\left({W}\mathrm{sSet}⟨{D},{C}⟩\right)={W}\left({E}\left(\mathrm{ndx}\right)\right)$
18 4 17 eqtr4d ${⊢}{W}\in \mathrm{V}\to {E}\left({W}\right)={E}\left({W}\mathrm{sSet}⟨{D},{C}⟩\right)$
19 1 str0 ${⊢}\varnothing ={E}\left(\varnothing \right)$
20 fvprc ${⊢}¬{W}\in \mathrm{V}\to {E}\left({W}\right)=\varnothing$
21 reldmsets ${⊢}\mathrm{Rel}\mathrm{dom}\mathrm{sSet}$
22 21 ovprc1 ${⊢}¬{W}\in \mathrm{V}\to {W}\mathrm{sSet}⟨{D},{C}⟩=\varnothing$
23 22 fveq2d ${⊢}¬{W}\in \mathrm{V}\to {E}\left({W}\mathrm{sSet}⟨{D},{C}⟩\right)={E}\left(\varnothing \right)$
24 19 20 23 3eqtr4a ${⊢}¬{W}\in \mathrm{V}\to {E}\left({W}\right)={E}\left({W}\mathrm{sSet}⟨{D},{C}⟩\right)$
25 18 24 pm2.61i ${⊢}{E}\left({W}\right)={E}\left({W}\mathrm{sSet}⟨{D},{C}⟩\right)$