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=SlotE⁡ndx
Assertion setsid ⊢W∈A∧C∈V→C=E⁡WsSetE⁡ndxC

Proof

Step Hyp Ref Expression
1 setsid.e ⊢E=SlotE⁡ndx
2 setsval ⊢W∈A∧C∈V→WsSetE⁡ndxC=W↾V∖E⁡ndx∪E⁡ndxC
3 2 fveq2d ⊢W∈A∧C∈V→E⁡WsSetE⁡ndxC=E⁡W↾V∖E⁡ndx∪E⁡ndxC
4 resexg ⊢W∈A→W↾V∖E⁡ndx∈V
5 4 adantr ⊢W∈A∧C∈V→W↾V∖E⁡ndx∈V
6 snex ⊢E⁡ndxC∈V
7 unexg ⊢W↾V∖E⁡ndx∈V∧E⁡ndxC∈V→W↾V∖E⁡ndx∪E⁡ndxC∈V
8 5 6 7 sylancl ⊢W∈A∧C∈V→W↾V∖E⁡ndx∪E⁡ndxC∈V
9 1 8 strfvnd ⊢W∈A∧C∈V→E⁡W↾V∖E⁡ndx∪E⁡ndxC=W↾V∖E⁡ndx∪E⁡ndxC⁡E⁡ndx
10 fvex ⊢E⁡ndx∈V
11 10 snid ⊢E⁡ndx∈E⁡ndx
12 fvres ⊢E⁡ndx∈E⁡ndx→W↾V∖E⁡ndx∪E⁡ndxC↾E⁡ndx⁡E⁡ndx=W↾V∖E⁡ndx∪E⁡ndxC⁡E⁡ndx
13 11 12 ax-mp ⊢W↾V∖E⁡ndx∪E⁡ndxC↾E⁡ndx⁡E⁡ndx=W↾V∖E⁡ndx∪E⁡ndxC⁡E⁡ndx
14 resres ⊢W↾V∖E⁡ndx↾E⁡ndx=W↾V∖E⁡ndx∩E⁡ndx
15 disjdifr ⊢V∖E⁡ndx∩E⁡ndx=∅
16 15 reseq2i ⊢W↾V∖E⁡ndx∩E⁡ndx=W↾∅
17 res0 ⊢W↾∅=∅
18 16 17 eqtri ⊢W↾V∖E⁡ndx∩E⁡ndx=∅
19 14 18 eqtri ⊢W↾V∖E⁡ndx↾E⁡ndx=∅
20 19 a1i ⊢W∈A∧C∈V→W↾V∖E⁡ndx↾E⁡ndx=∅
21 elex ⊢C∈V→C∈V
22 21 adantl ⊢W∈A∧C∈V→C∈V
23 opelxpi ⊢E⁡ndx∈V∧C∈V→E⁡ndxC∈V×V
24 10 22 23 sylancr ⊢W∈A∧C∈V→E⁡ndxC∈V×V
25 opex ⊢E⁡ndxC∈V
26 25 relsn ⊢Rel⁡E⁡ndxC↔E⁡ndxC∈V×V
27 24 26 sylibr ⊢W∈A∧C∈V→Rel⁡E⁡ndxC
28 dmsnopss ⊢dom⁡E⁡ndxC⊆E⁡ndx
29 relssres ⊢Rel⁡E⁡ndxC∧dom⁡E⁡ndxC⊆E⁡ndx→E⁡ndxC↾E⁡ndx=E⁡ndxC
30 27 28 29 sylancl ⊢W∈A∧C∈V→E⁡ndxC↾E⁡ndx=E⁡ndxC
31 20 30 uneq12d ⊢W∈A∧C∈V→W↾V∖E⁡ndx↾E⁡ndx∪E⁡ndxC↾E⁡ndx=∅∪E⁡ndxC
32 resundir ⊢W↾V∖E⁡ndx∪E⁡ndxC↾E⁡ndx=W↾V∖E⁡ndx↾E⁡ndx∪E⁡ndxC↾E⁡ndx
33 un0 ⊢E⁡ndxC∪∅=E⁡ndxC
34 uncom ⊢E⁡ndxC∪∅=∅∪E⁡ndxC
35 33 34 eqtr3i ⊢E⁡ndxC=∅∪E⁡ndxC
36 31 32 35 3eqtr4g ⊢W∈A∧C∈V→W↾V∖E⁡ndx∪E⁡ndxC↾E⁡ndx=E⁡ndxC
37 36 fveq1d ⊢W∈A∧C∈V→W↾V∖E⁡ndx∪E⁡ndxC↾E⁡ndx⁡E⁡ndx=E⁡ndxC⁡E⁡ndx
38 13 37 eqtr3id ⊢W∈A∧C∈V→W↾V∖E⁡ndx∪E⁡ndxC⁡E⁡ndx=E⁡ndxC⁡E⁡ndx
39 10 a1i ⊢W∈A∧C∈V→E⁡ndx∈V
40 fvsng ⊢E⁡ndx∈V∧C∈V→E⁡ndxC⁡E⁡ndx=C
41 39 40 sylancom ⊢W∈A∧C∈V→E⁡ndxC⁡E⁡ndx=C
42 38 41 eqtrd ⊢W∈A∧C∈V→W↾V∖E⁡ndx∪E⁡ndxC⁡E⁡ndx=C
43 3 9 42 3eqtrrd ⊢W∈A∧C∈V→C=E⁡WsSetE⁡ndxC