Metamath Proof Explorer


Theorem setsnidOLD

Description: Obsolete proof of setsnid as of 7-Nov-2024. Value of the structure replacement function at an untouched index. (Contributed by Mario Carneiro, 1-Dec-2014) (Revised by Mario Carneiro, 30-Apr-2015) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses setsid.e
|- E = Slot ( E ` ndx )
setsnid.n
|- ( E ` ndx ) =/= D
Assertion setsnidOLD
|- ( 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 fvprc
 |-  ( -. W e. _V -> ( E ` W ) = (/) )
21 reldmsets
 |-  Rel dom sSet
22 21 ovprc1
 |-  ( -. W e. _V -> ( W sSet <. D , C >. ) = (/) )
23 22 fveq2d
 |-  ( -. W e. _V -> ( E ` ( W sSet <. D , C >. ) ) = ( E ` (/) ) )
24 19 20 23 3eqtr4a
 |-  ( -. W e. _V -> ( E ` W ) = ( E ` ( W sSet <. D , C >. ) ) )
25 18 24 pm2.61i
 |-  ( E ` W ) = ( E ` ( W sSet <. D , C >. ) )