Metamath Proof Explorer

Theorem setsnid

Description: Value of the structure replacement function at an untouched index. (Contributed by Mario Carneiro, 1-Dec-2014) (Revised by Mario Carneiro, 30-Apr-2015) (Proof shortened by AV, 7-Nov-2024)

Ref Expression
Hypotheses setsid.e 
|- E = Slot ( E ` ndx )
setsnid.n 
|- ( E ` ndx ) =/= D
Assertion setsnid 
|- ( E ` W ) = ( E ` ( W sSet <. D , C >. ) )

Proof

Step Hyp Ref Expression
1 setsid.e 
 |-  E = Slot ( E ` ndx )
2 setsnid.n 
 |-  ( E ` ndx ) =/= D
3 id 
 |-  ( W e. _V -> W e. _V )
4 1 3 strfvnd 
 |-  ( W e. _V -> ( E ` W ) = ( W ` ( E ` ndx ) ) )
5 ovex 
 |-  ( W sSet <. D , C >. ) e. _V
6 5 1 strfvn 
 |-  ( E ` ( W sSet <. D , C >. ) ) = ( ( W sSet <. D , C >. ) ` ( E ` ndx ) )
7 setsres 
 |-  ( W e. _V -> ( ( W sSet <. D , C >. ) |` ( _V \ { D } ) ) = ( W |` ( _V \ { D } ) ) )
8 7 fveq1d 
 |-  ( W e. _V -> ( ( ( W sSet <. D , C >. ) |` ( _V \ { D } ) ) ` ( E ` ndx ) ) = ( ( W |` ( _V \ { D } ) ) ` ( E ` ndx ) ) )
9 fvex 
 |-  ( E ` ndx ) e. _V
10 eldifsn 
 |-  ( ( E ` ndx ) e. ( _V \ { D } ) <-> ( ( E ` ndx ) e. _V /\ ( E ` ndx ) =/= D ) )
11 9 2 10 mpbir2an 
 |-  ( E ` ndx ) e. ( _V \ { D } )
12 fvres 
 |-  ( ( E ` ndx ) e. ( _V \ { D } ) -> ( ( ( W sSet <. D , C >. ) |` ( _V \ { D } ) ) ` ( E ` ndx ) ) = ( ( W sSet <. D , C >. ) ` ( E ` ndx ) ) )
13 11 12 ax-mp 
 |-  ( ( ( W sSet <. D , C >. ) |` ( _V \ { D } ) ) ` ( E ` ndx ) ) = ( ( W sSet <. D , C >. ) ` ( E ` ndx ) )
14 fvres 
 |-  ( ( E ` ndx ) e. ( _V \ { D } ) -> ( ( W |` ( _V \ { D } ) ) ` ( E ` ndx ) ) = ( W ` ( E ` ndx ) ) )
15 11 14 ax-mp 
 |-  ( ( W |` ( _V \ { D } ) ) ` ( E ` ndx ) ) = ( W ` ( E ` ndx ) )
16 8 13 15 3eqtr3g 
 |-  ( W e. _V -> ( ( W sSet <. D , C >. ) ` ( E ` ndx ) ) = ( W ` ( E ` ndx ) ) )
17 6 16 eqtrid 
 |-  ( W e. _V -> ( E ` ( W sSet <. D , C >. ) ) = ( W ` ( E ` ndx ) ) )
18 4 17 eqtr4d 
 |-  ( W e. _V -> ( E ` W ) = ( E ` ( W sSet <. D , C >. ) ) )
19 1 str0 
 |-  (/) = ( E ` (/) )
20 19 eqcomi 
 |-  ( E ` (/) ) = (/)
21 eqid 
 |-  ( W sSet <. D , C >. ) = ( W sSet <. D , C >. )
22 reldmsets 
 |-  Rel dom sSet
23 20 21 22 oveqprc 
 |-  ( -. W e. _V -> ( E ` W ) = ( E ` ( W sSet <. D , C >. ) ) )
24 18 23 pm2.61i 
 |-  ( E ` W ) = ( E ` ( W sSet <. D , C >. ) )