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 ⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
Assertion setsid ( ( 𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → 𝐶 = ( 𝐸 ‘ ( 𝑊 sSet ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ) ) )

Proof

Step Hyp Ref Expression
1 setsid.e ⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
2 setsval ⊢ ( ( 𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → ( 𝑊 sSet ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ) = ( ( 𝑊 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ∪ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ) )
3 2 fveq2d ⊢ ( ( 𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐸 ‘ ( 𝑊 sSet ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ) ) = ( 𝐸 ‘ ( ( 𝑊 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ∪ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ) ) )
4 resexg ⊢ ( 𝑊 ∈ 𝐴 → ( 𝑊 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ∈ V )
5 4 adantr ⊢ ( ( 𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → ( 𝑊 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ∈ V )
6 snex ⊢ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ∈ V
7 unexg ⊢ ( ( ( 𝑊 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ∈ V ∧ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ∈ V ) → ( ( 𝑊 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ∪ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ) ∈ V )
8 5 6 7 sylancl ⊢ ( ( 𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → ( ( 𝑊 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ∪ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ) ∈ V )
9 1 8 strfvnd ⊢ ( ( 𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐸 ‘ ( ( 𝑊 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ∪ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ) ) = ( ( ( 𝑊 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ∪ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ) ‘ ( 𝐸 ‘ ndx ) ) )
10 fvex ⊢ ( 𝐸 ‘ ndx ) ∈ V
11 10 snid ⊢ ( 𝐸 ‘ ndx ) ∈ { ( 𝐸 ‘ ndx ) }
12 fvres ⊢ ( ( 𝐸 ‘ ndx ) ∈ { ( 𝐸 ‘ ndx ) } → ( ( ( ( 𝑊 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ∪ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ) ↾ { ( 𝐸 ‘ ndx ) } ) ‘ ( 𝐸 ‘ ndx ) ) = ( ( ( 𝑊 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ∪ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ) ‘ ( 𝐸 ‘ ndx ) ) )
13 11 12 ax-mp ⊢ ( ( ( ( 𝑊 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ∪ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ) ↾ { ( 𝐸 ‘ ndx ) } ) ‘ ( 𝐸 ‘ ndx ) ) = ( ( ( 𝑊 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ∪ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ) ‘ ( 𝐸 ‘ ndx ) )
14 resres ⊢ ( ( 𝑊 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ↾ { ( 𝐸 ‘ ndx ) } ) = ( 𝑊 ↾ ( ( V ∖ { ( 𝐸 ‘ ndx ) } ) ∩ { ( 𝐸 ‘ ndx ) } ) )
15 incom ⊢ ( ( V ∖ { ( 𝐸 ‘ ndx ) } ) ∩ { ( 𝐸 ‘ ndx ) } ) = ( { ( 𝐸 ‘ ndx ) } ∩ ( V ∖ { ( 𝐸 ‘ ndx ) } ) )
16 disjdif ⊢ ( { ( 𝐸 ‘ ndx ) } ∩ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) = ∅
17 15 16 eqtri ⊢ ( ( V ∖ { ( 𝐸 ‘ ndx ) } ) ∩ { ( 𝐸 ‘ ndx ) } ) = ∅
18 17 reseq2i ⊢ ( 𝑊 ↾ ( ( V ∖ { ( 𝐸 ‘ ndx ) } ) ∩ { ( 𝐸 ‘ ndx ) } ) ) = ( 𝑊 ↾ ∅ )
19 res0 ⊢ ( 𝑊 ↾ ∅ ) = ∅
20 18 19 eqtri ⊢ ( 𝑊 ↾ ( ( V ∖ { ( 𝐸 ‘ ndx ) } ) ∩ { ( 𝐸 ‘ ndx ) } ) ) = ∅
21 14 20 eqtri ⊢ ( ( 𝑊 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ↾ { ( 𝐸 ‘ ndx ) } ) = ∅
22 21 a1i ⊢ ( ( 𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → ( ( 𝑊 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ↾ { ( 𝐸 ‘ ndx ) } ) = ∅ )
23 elex ⊢ ( 𝐶 ∈ 𝑉 → 𝐶 ∈ V )
24 23 adantl ⊢ ( ( 𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → 𝐶 ∈ V )
25 opelxpi ⊢ ( ( ( 𝐸 ‘ ndx ) ∈ V ∧ 𝐶 ∈ V ) → ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ∈ ( V × V ) )
26 10 24 25 sylancr ⊢ ( ( 𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ∈ ( V × V ) )
27 opex ⊢ ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ∈ V
28 27 relsn ⊢ ( Rel { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ↔ ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ∈ ( V × V ) )
29 26 28 sylibr ⊢ ( ( 𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → Rel { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } )
30 dmsnopss ⊢ dom { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ⊆ { ( 𝐸 ‘ ndx ) }
31 relssres ⊢ ( ( Rel { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ∧ dom { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ⊆ { ( 𝐸 ‘ ndx ) } ) → ( { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ↾ { ( 𝐸 ‘ ndx ) } ) = { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } )
32 29 30 31 sylancl ⊢ ( ( 𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → ( { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ↾ { ( 𝐸 ‘ ndx ) } ) = { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } )
33 22 32 uneq12d ⊢ ( ( 𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → ( ( ( 𝑊 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ↾ { ( 𝐸 ‘ ndx ) } ) ∪ ( { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ↾ { ( 𝐸 ‘ ndx ) } ) ) = ( ∅ ∪ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ) )
34 resundir ⊢ ( ( ( 𝑊 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ∪ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ) ↾ { ( 𝐸 ‘ ndx ) } ) = ( ( ( 𝑊 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ↾ { ( 𝐸 ‘ ndx ) } ) ∪ ( { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ↾ { ( 𝐸 ‘ ndx ) } ) )
35 un0 ⊢ ( { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ∪ ∅ ) = { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ }
36 uncom ⊢ ( { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ∪ ∅ ) = ( ∅ ∪ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } )
37 35 36 eqtr3i ⊢ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } = ( ∅ ∪ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } )
38 33 34 37 3eqtr4g ⊢ ( ( 𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → ( ( ( 𝑊 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ∪ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ) ↾ { ( 𝐸 ‘ ndx ) } ) = { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } )
39 38 fveq1d ⊢ ( ( 𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → ( ( ( ( 𝑊 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ∪ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ) ↾ { ( 𝐸 ‘ ndx ) } ) ‘ ( 𝐸 ‘ ndx ) ) = ( { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ‘ ( 𝐸 ‘ ndx ) ) )
40 13 39 eqtr3id ⊢ ( ( 𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → ( ( ( 𝑊 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ∪ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ) ‘ ( 𝐸 ‘ ndx ) ) = ( { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ‘ ( 𝐸 ‘ ndx ) ) )
41 10 a1i ⊢ ( ( 𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐸 ‘ ndx ) ∈ V )
42 fvsng ⊢ ( ( ( 𝐸 ‘ ndx ) ∈ V ∧ 𝐶 ∈ 𝑉 ) → ( { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ‘ ( 𝐸 ‘ ndx ) ) = 𝐶 )
43 41 42 sylancom ⊢ ( ( 𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → ( { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ‘ ( 𝐸 ‘ ndx ) ) = 𝐶 )
44 40 43 eqtrd ⊢ ( ( 𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → ( ( ( 𝑊 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ∪ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ) ‘ ( 𝐸 ‘ ndx ) ) = 𝐶 )
45 3 9 44 3eqtrrd ⊢ ( ( 𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → 𝐶 = ( 𝐸 ‘ ( 𝑊 sSet ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ) ) )