# Metamath Proof Explorer

## Theorem setsid

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)

Ref Expression
Hypothesis setsid.e ${⊢}{E}=\mathrm{Slot}{E}\left(\mathrm{ndx}\right)$
Assertion setsid ${⊢}\left({W}\in {A}\wedge {C}\in {V}\right)\to {C}={E}\left({W}\mathrm{sSet}⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right)$

### Proof

Step Hyp Ref Expression
1 setsid.e ${⊢}{E}=\mathrm{Slot}{E}\left(\mathrm{ndx}\right)$
2 setsval ${⊢}\left({W}\in {A}\wedge {C}\in {V}\right)\to {W}\mathrm{sSet}⟨{E}\left(\mathrm{ndx}\right),{C}⟩=\left({{W}↾}_{\left(\mathrm{V}\setminus \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)}\right)\cup \left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}$
3 2 fveq2d ${⊢}\left({W}\in {A}\wedge {C}\in {V}\right)\to {E}\left({W}\mathrm{sSet}⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right)={E}\left(\left({{W}↾}_{\left(\mathrm{V}\setminus \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)}\right)\cup \left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}\right)$
4 resexg ${⊢}{W}\in {A}\to {{W}↾}_{\left(\mathrm{V}\setminus \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)}\in \mathrm{V}$
5 4 adantr ${⊢}\left({W}\in {A}\wedge {C}\in {V}\right)\to {{W}↾}_{\left(\mathrm{V}\setminus \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)}\in \mathrm{V}$
6 snex ${⊢}\left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}\in \mathrm{V}$
7 unexg ${⊢}\left({{W}↾}_{\left(\mathrm{V}\setminus \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)}\in \mathrm{V}\wedge \left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}\in \mathrm{V}\right)\to \left({{W}↾}_{\left(\mathrm{V}\setminus \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)}\right)\cup \left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}\in \mathrm{V}$
8 5 6 7 sylancl ${⊢}\left({W}\in {A}\wedge {C}\in {V}\right)\to \left({{W}↾}_{\left(\mathrm{V}\setminus \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)}\right)\cup \left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}\in \mathrm{V}$
9 1 8 strfvnd ${⊢}\left({W}\in {A}\wedge {C}\in {V}\right)\to {E}\left(\left({{W}↾}_{\left(\mathrm{V}\setminus \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)}\right)\cup \left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}\right)=\left(\left({{W}↾}_{\left(\mathrm{V}\setminus \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)}\right)\cup \left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}\right)\left({E}\left(\mathrm{ndx}\right)\right)$
10 fvex ${⊢}{E}\left(\mathrm{ndx}\right)\in \mathrm{V}$
11 10 snid ${⊢}{E}\left(\mathrm{ndx}\right)\in \left\{{E}\left(\mathrm{ndx}\right)\right\}$
12 fvres ${⊢}{E}\left(\mathrm{ndx}\right)\in \left\{{E}\left(\mathrm{ndx}\right)\right\}\to \left({\left(\left({{W}↾}_{\left(\mathrm{V}\setminus \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)}\right)\cup \left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}\right)↾}_{\left\{{E}\left(\mathrm{ndx}\right)\right\}}\right)\left({E}\left(\mathrm{ndx}\right)\right)=\left(\left({{W}↾}_{\left(\mathrm{V}\setminus \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)}\right)\cup \left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}\right)\left({E}\left(\mathrm{ndx}\right)\right)$
13 11 12 ax-mp ${⊢}\left({\left(\left({{W}↾}_{\left(\mathrm{V}\setminus \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)}\right)\cup \left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}\right)↾}_{\left\{{E}\left(\mathrm{ndx}\right)\right\}}\right)\left({E}\left(\mathrm{ndx}\right)\right)=\left(\left({{W}↾}_{\left(\mathrm{V}\setminus \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)}\right)\cup \left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}\right)\left({E}\left(\mathrm{ndx}\right)\right)$
14 resres ${⊢}{\left({{W}↾}_{\left(\mathrm{V}\setminus \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)}\right)↾}_{\left\{{E}\left(\mathrm{ndx}\right)\right\}}={{W}↾}_{\left(\left(\mathrm{V}\setminus \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)\cap \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)}$
15 incom ${⊢}\left(\mathrm{V}\setminus \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)\cap \left\{{E}\left(\mathrm{ndx}\right)\right\}=\left\{{E}\left(\mathrm{ndx}\right)\right\}\cap \left(\mathrm{V}\setminus \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)$
16 disjdif ${⊢}\left\{{E}\left(\mathrm{ndx}\right)\right\}\cap \left(\mathrm{V}\setminus \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)=\varnothing$
17 15 16 eqtri ${⊢}\left(\mathrm{V}\setminus \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)\cap \left\{{E}\left(\mathrm{ndx}\right)\right\}=\varnothing$
18 17 reseq2i ${⊢}{{W}↾}_{\left(\left(\mathrm{V}\setminus \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)\cap \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)}={{W}↾}_{\varnothing }$
19 res0 ${⊢}{{W}↾}_{\varnothing }=\varnothing$
20 18 19 eqtri ${⊢}{{W}↾}_{\left(\left(\mathrm{V}\setminus \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)\cap \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)}=\varnothing$
21 14 20 eqtri ${⊢}{\left({{W}↾}_{\left(\mathrm{V}\setminus \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)}\right)↾}_{\left\{{E}\left(\mathrm{ndx}\right)\right\}}=\varnothing$
22 21 a1i ${⊢}\left({W}\in {A}\wedge {C}\in {V}\right)\to {\left({{W}↾}_{\left(\mathrm{V}\setminus \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)}\right)↾}_{\left\{{E}\left(\mathrm{ndx}\right)\right\}}=\varnothing$
23 elex ${⊢}{C}\in {V}\to {C}\in \mathrm{V}$
24 23 adantl ${⊢}\left({W}\in {A}\wedge {C}\in {V}\right)\to {C}\in \mathrm{V}$
25 opelxpi ${⊢}\left({E}\left(\mathrm{ndx}\right)\in \mathrm{V}\wedge {C}\in \mathrm{V}\right)\to ⟨{E}\left(\mathrm{ndx}\right),{C}⟩\in \left(\mathrm{V}×\mathrm{V}\right)$
26 10 24 25 sylancr ${⊢}\left({W}\in {A}\wedge {C}\in {V}\right)\to ⟨{E}\left(\mathrm{ndx}\right),{C}⟩\in \left(\mathrm{V}×\mathrm{V}\right)$
27 opex ${⊢}⟨{E}\left(\mathrm{ndx}\right),{C}⟩\in \mathrm{V}$
28 27 relsn ${⊢}\mathrm{Rel}\left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}↔⟨{E}\left(\mathrm{ndx}\right),{C}⟩\in \left(\mathrm{V}×\mathrm{V}\right)$
29 26 28 sylibr ${⊢}\left({W}\in {A}\wedge {C}\in {V}\right)\to \mathrm{Rel}\left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}$
30 dmsnopss ${⊢}\mathrm{dom}\left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}\subseteq \left\{{E}\left(\mathrm{ndx}\right)\right\}$
31 relssres ${⊢}\left(\mathrm{Rel}\left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}\wedge \mathrm{dom}\left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}\subseteq \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)\to {\left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}↾}_{\left\{{E}\left(\mathrm{ndx}\right)\right\}}=\left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}$
32 29 30 31 sylancl ${⊢}\left({W}\in {A}\wedge {C}\in {V}\right)\to {\left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}↾}_{\left\{{E}\left(\mathrm{ndx}\right)\right\}}=\left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}$
33 22 32 uneq12d ${⊢}\left({W}\in {A}\wedge {C}\in {V}\right)\to \left({\left({{W}↾}_{\left(\mathrm{V}\setminus \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)}\right)↾}_{\left\{{E}\left(\mathrm{ndx}\right)\right\}}\right)\cup \left({\left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}↾}_{\left\{{E}\left(\mathrm{ndx}\right)\right\}}\right)=\varnothing \cup \left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}$
34 resundir ${⊢}{\left(\left({{W}↾}_{\left(\mathrm{V}\setminus \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)}\right)\cup \left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}\right)↾}_{\left\{{E}\left(\mathrm{ndx}\right)\right\}}=\left({\left({{W}↾}_{\left(\mathrm{V}\setminus \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)}\right)↾}_{\left\{{E}\left(\mathrm{ndx}\right)\right\}}\right)\cup \left({\left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}↾}_{\left\{{E}\left(\mathrm{ndx}\right)\right\}}\right)$
35 un0 ${⊢}\left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}\cup \varnothing =\left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}$
36 uncom ${⊢}\left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}\cup \varnothing =\varnothing \cup \left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}$
37 35 36 eqtr3i ${⊢}\left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}=\varnothing \cup \left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}$
38 33 34 37 3eqtr4g ${⊢}\left({W}\in {A}\wedge {C}\in {V}\right)\to {\left(\left({{W}↾}_{\left(\mathrm{V}\setminus \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)}\right)\cup \left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}\right)↾}_{\left\{{E}\left(\mathrm{ndx}\right)\right\}}=\left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}$
39 38 fveq1d ${⊢}\left({W}\in {A}\wedge {C}\in {V}\right)\to \left({\left(\left({{W}↾}_{\left(\mathrm{V}\setminus \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)}\right)\cup \left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}\right)↾}_{\left\{{E}\left(\mathrm{ndx}\right)\right\}}\right)\left({E}\left(\mathrm{ndx}\right)\right)=\left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}\left({E}\left(\mathrm{ndx}\right)\right)$
40 13 39 syl5eqr ${⊢}\left({W}\in {A}\wedge {C}\in {V}\right)\to \left(\left({{W}↾}_{\left(\mathrm{V}\setminus \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)}\right)\cup \left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}\right)\left({E}\left(\mathrm{ndx}\right)\right)=\left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}\left({E}\left(\mathrm{ndx}\right)\right)$
41 10 a1i ${⊢}\left({W}\in {A}\wedge {C}\in {V}\right)\to {E}\left(\mathrm{ndx}\right)\in \mathrm{V}$
42 fvsng ${⊢}\left({E}\left(\mathrm{ndx}\right)\in \mathrm{V}\wedge {C}\in {V}\right)\to \left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}\left({E}\left(\mathrm{ndx}\right)\right)={C}$
43 41 42 sylancom ${⊢}\left({W}\in {A}\wedge {C}\in {V}\right)\to \left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}\left({E}\left(\mathrm{ndx}\right)\right)={C}$
44 40 43 eqtrd ${⊢}\left({W}\in {A}\wedge {C}\in {V}\right)\to \left(\left({{W}↾}_{\left(\mathrm{V}\setminus \left\{{E}\left(\mathrm{ndx}\right)\right\}\right)}\right)\cup \left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}\right)\left({E}\left(\mathrm{ndx}\right)\right)={C}$
45 3 9 44 3eqtrrd ${⊢}\left({W}\in {A}\wedge {C}\in {V}\right)\to {C}={E}\left({W}\mathrm{sSet}⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right)$