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

Proof

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