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 disjdifr ⊢ ( ( V ∖ { ( 𝐸 ‘ ndx ) } ) ∩ { ( 𝐸 ‘ ndx ) } ) = ∅
16 15 reseq2i ⊢ ( 𝑊 ↾ ( ( V ∖ { ( 𝐸 ‘ ndx ) } ) ∩ { ( 𝐸 ‘ ndx ) } ) ) = ( 𝑊 ↾ ∅ )
17 res0 ⊢ ( 𝑊 ↾ ∅ ) = ∅
18 16 17 eqtri ⊢ ( 𝑊 ↾ ( ( V ∖ { ( 𝐸 ‘ ndx ) } ) ∩ { ( 𝐸 ‘ ndx ) } ) ) = ∅
19 14 18 eqtri ⊢ ( ( 𝑊 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ↾ { ( 𝐸 ‘ ndx ) } ) = ∅
20 19 a1i ⊢ ( ( 𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → ( ( 𝑊 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ↾ { ( 𝐸 ‘ ndx ) } ) = ∅ )
21 elex ⊢ ( 𝐶 ∈ 𝑉 → 𝐶 ∈ V )
22 21 adantl ⊢ ( ( 𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → 𝐶 ∈ V )
23 opelxpi ⊢ ( ( ( 𝐸 ‘ ndx ) ∈ V ∧ 𝐶 ∈ V ) → ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ∈ ( V × V ) )
24 10 22 23 sylancr ⊢ ( ( 𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ∈ ( V × V ) )
25 opex ⊢ ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ∈ V
26 25 relsn ⊢ ( Rel { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ↔ ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ∈ ( V × V ) )
27 24 26 sylibr ⊢ ( ( 𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → Rel { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } )
28 dmsnopss ⊢ dom { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ⊆ { ( 𝐸 ‘ ndx ) }
29 relssres ⊢ ( ( Rel { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ∧ dom { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ⊆ { ( 𝐸 ‘ ndx ) } ) → ( { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ↾ { ( 𝐸 ‘ ndx ) } ) = { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } )
30 27 28 29 sylancl ⊢ ( ( 𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → ( { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ↾ { ( 𝐸 ‘ ndx ) } ) = { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } )
31 20 30 uneq12d ⊢ ( ( 𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → ( ( ( 𝑊 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ↾ { ( 𝐸 ‘ ndx ) } ) ∪ ( { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ↾ { ( 𝐸 ‘ ndx ) } ) ) = ( ∅ ∪ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ) )
32 resundir ⊢ ( ( ( 𝑊 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ∪ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ) ↾ { ( 𝐸 ‘ ndx ) } ) = ( ( ( 𝑊 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ↾ { ( 𝐸 ‘ ndx ) } ) ∪ ( { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ↾ { ( 𝐸 ‘ ndx ) } ) )
33 un0 ⊢ ( { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ∪ ∅ ) = { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ }
34 uncom ⊢ ( { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ∪ ∅ ) = ( ∅ ∪ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } )
35 33 34 eqtr3i ⊢ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } = ( ∅ ∪ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } )
36 31 32 35 3eqtr4g ⊢ ( ( 𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → ( ( ( 𝑊 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ∪ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ) ↾ { ( 𝐸 ‘ ndx ) } ) = { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } )
37 36 fveq1d ⊢ ( ( 𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → ( ( ( ( 𝑊 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ∪ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ) ↾ { ( 𝐸 ‘ ndx ) } ) ‘ ( 𝐸 ‘ ndx ) ) = ( { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ‘ ( 𝐸 ‘ ndx ) ) )
38 13 37 eqtr3id ⊢ ( ( 𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → ( ( ( 𝑊 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ∪ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ) ‘ ( 𝐸 ‘ ndx ) ) = ( { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ‘ ( 𝐸 ‘ ndx ) ) )
39 10 a1i ⊢ ( ( 𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐸 ‘ ndx ) ∈ V )
40 fvsng ⊢ ( ( ( 𝐸 ‘ ndx ) ∈ V ∧ 𝐶 ∈ 𝑉 ) → ( { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ‘ ( 𝐸 ‘ ndx ) ) = 𝐶 )
41 39 40 sylancom ⊢ ( ( 𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → ( { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ‘ ( 𝐸 ‘ ndx ) ) = 𝐶 )
42 38 41 eqtrd ⊢ ( ( 𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → ( ( ( 𝑊 ↾ ( V ∖ { ( 𝐸 ‘ ndx ) } ) ) ∪ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ) ‘ ( 𝐸 ‘ ndx ) ) = 𝐶 )
43 3 9 42 3eqtrrd ⊢ ( ( 𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → 𝐶 = ( 𝐸 ‘ ( 𝑊 sSet ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ) ) )