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 e. A /\ C e. V ) -> C = ( E ` ( W sSet <. ( E ` ndx ) , C >. ) ) )

Proof

Step Hyp Ref Expression
1 setsid.e 
 |-  E = Slot ( E ` ndx )
2 setsval 
 |-  ( ( W e. A /\ C e. V ) -> ( W sSet <. ( E ` ndx ) , C >. ) = ( ( W |` ( _V \ { ( E ` ndx ) } ) ) u. { <. ( E ` ndx ) , C >. } ) )
3 2 fveq2d 
 |-  ( ( W e. A /\ C e. V ) -> ( E ` ( W sSet <. ( E ` ndx ) , C >. ) ) = ( E ` ( ( W |` ( _V \ { ( E ` ndx ) } ) ) u. { <. ( E ` ndx ) , C >. } ) ) )
4 resexg 
 |-  ( W e. A -> ( W |` ( _V \ { ( E ` ndx ) } ) ) e. _V )
5 4 adantr 
 |-  ( ( W e. A /\ C e. V ) -> ( W |` ( _V \ { ( E ` ndx ) } ) ) e. _V )
6 snex 
 |-  { <. ( E ` ndx ) , C >. } e. _V
7 unexg 
 |-  ( ( ( W |` ( _V \ { ( E ` ndx ) } ) ) e. _V /\ { <. ( E ` ndx ) , C >. } e. _V ) -> ( ( W |` ( _V \ { ( E ` ndx ) } ) ) u. { <. ( E ` ndx ) , C >. } ) e. _V )
8 5 6 7 sylancl 
 |-  ( ( W e. A /\ C e. V ) -> ( ( W |` ( _V \ { ( E ` ndx ) } ) ) u. { <. ( E ` ndx ) , C >. } ) e. _V )
9 1 8 strfvnd 
 |-  ( ( W e. A /\ C e. V ) -> ( E ` ( ( W |` ( _V \ { ( E ` ndx ) } ) ) u. { <. ( E ` ndx ) , C >. } ) ) = ( ( ( W |` ( _V \ { ( E ` ndx ) } ) ) u. { <. ( E ` ndx ) , C >. } ) ` ( E ` ndx ) ) )
10 fvex 
 |-  ( E ` ndx ) e. _V
11 10 snid 
 |-  ( E ` ndx ) e. { ( E ` ndx ) }
12 fvres 
 |-  ( ( E ` ndx ) e. { ( E ` ndx ) } -> ( ( ( ( W |` ( _V \ { ( E ` ndx ) } ) ) u. { <. ( E ` ndx ) , C >. } ) |` { ( E ` ndx ) } ) ` ( E ` ndx ) ) = ( ( ( W |` ( _V \ { ( E ` ndx ) } ) ) u. { <. ( E ` ndx ) , C >. } ) ` ( E ` ndx ) ) )
13 11 12 ax-mp 
 |-  ( ( ( ( W |` ( _V \ { ( E ` ndx ) } ) ) u. { <. ( E ` ndx ) , C >. } ) |` { ( E ` ndx ) } ) ` ( E ` ndx ) ) = ( ( ( W |` ( _V \ { ( E ` ndx ) } ) ) u. { <. ( E ` ndx ) , C >. } ) ` ( E ` ndx ) )
14 resres 
 |-  ( ( W |` ( _V \ { ( E ` ndx ) } ) ) |` { ( E ` ndx ) } ) = ( W |` ( ( _V \ { ( E ` ndx ) } ) i^i { ( E ` ndx ) } ) )
15 disjdifr 
 |-  ( ( _V \ { ( E ` ndx ) } ) i^i { ( E ` ndx ) } ) = (/)
16 15 reseq2i 
 |-  ( W |` ( ( _V \ { ( E ` ndx ) } ) i^i { ( E ` ndx ) } ) ) = ( W |` (/) )
17 res0 
 |-  ( W |` (/) ) = (/)
18 16 17 eqtri 
 |-  ( W |` ( ( _V \ { ( E ` ndx ) } ) i^i { ( E ` ndx ) } ) ) = (/)
19 14 18 eqtri 
 |-  ( ( W |` ( _V \ { ( E ` ndx ) } ) ) |` { ( E ` ndx ) } ) = (/)
20 19 a1i 
 |-  ( ( W e. A /\ C e. V ) -> ( ( W |` ( _V \ { ( E ` ndx ) } ) ) |` { ( E ` ndx ) } ) = (/) )
21 elex 
 |-  ( C e. V -> C e. _V )
22 21 adantl 
 |-  ( ( W e. A /\ C e. V ) -> C e. _V )
23 opelxpi 
 |-  ( ( ( E ` ndx ) e. _V /\ C e. _V ) -> <. ( E ` ndx ) , C >. e. ( _V X. _V ) )
24 10 22 23 sylancr 
 |-  ( ( W e. A /\ C e. V ) -> <. ( E ` ndx ) , C >. e. ( _V X. _V ) )
25 opex 
 |-  <. ( E ` ndx ) , C >. e. _V
26 25 relsn 
 |-  ( Rel { <. ( E ` ndx ) , C >. } <-> <. ( E ` ndx ) , C >. e. ( _V X. _V ) )
27 24 26 sylibr 
 |-  ( ( W e. A /\ C e. V ) -> Rel { <. ( E ` ndx ) , C >. } )
28 dmsnopss 
 |-  dom { <. ( E ` ndx ) , C >. } C_ { ( E ` ndx ) }
29 relssres 
 |-  ( ( Rel { <. ( E ` ndx ) , C >. } /\ dom { <. ( E ` ndx ) , C >. } C_ { ( E ` ndx ) } ) -> ( { <. ( E ` ndx ) , C >. } |` { ( E ` ndx ) } ) = { <. ( E ` ndx ) , C >. } )
30 27 28 29 sylancl 
 |-  ( ( W e. A /\ C e. V ) -> ( { <. ( E ` ndx ) , C >. } |` { ( E ` ndx ) } ) = { <. ( E ` ndx ) , C >. } )
31 20 30 uneq12d 
 |-  ( ( W e. A /\ C e. V ) -> ( ( ( W |` ( _V \ { ( E ` ndx ) } ) ) |` { ( E ` ndx ) } ) u. ( { <. ( E ` ndx ) , C >. } |` { ( E ` ndx ) } ) ) = ( (/) u. { <. ( E ` ndx ) , C >. } ) )
32 resundir 
 |-  ( ( ( W |` ( _V \ { ( E ` ndx ) } ) ) u. { <. ( E ` ndx ) , C >. } ) |` { ( E ` ndx ) } ) = ( ( ( W |` ( _V \ { ( E ` ndx ) } ) ) |` { ( E ` ndx ) } ) u. ( { <. ( E ` ndx ) , C >. } |` { ( E ` ndx ) } ) )
33 un0 
 |-  ( { <. ( E ` ndx ) , C >. } u. (/) ) = { <. ( E ` ndx ) , C >. }
34 uncom 
 |-  ( { <. ( E ` ndx ) , C >. } u. (/) ) = ( (/) u. { <. ( E ` ndx ) , C >. } )
35 33 34 eqtr3i 
 |-  { <. ( E ` ndx ) , C >. } = ( (/) u. { <. ( E ` ndx ) , C >. } )
36 31 32 35 3eqtr4g 
 |-  ( ( W e. A /\ C e. V ) -> ( ( ( W |` ( _V \ { ( E ` ndx ) } ) ) u. { <. ( E ` ndx ) , C >. } ) |` { ( E ` ndx ) } ) = { <. ( E ` ndx ) , C >. } )
37 36 fveq1d 
 |-  ( ( W e. A /\ C e. V ) -> ( ( ( ( W |` ( _V \ { ( E ` ndx ) } ) ) u. { <. ( E ` ndx ) , C >. } ) |` { ( E ` ndx ) } ) ` ( E ` ndx ) ) = ( { <. ( E ` ndx ) , C >. } ` ( E ` ndx ) ) )
38 13 37 eqtr3id 
 |-  ( ( W e. A /\ C e. V ) -> ( ( ( W |` ( _V \ { ( E ` ndx ) } ) ) u. { <. ( E ` ndx ) , C >. } ) ` ( E ` ndx ) ) = ( { <. ( E ` ndx ) , C >. } ` ( E ` ndx ) ) )
39 10 a1i 
 |-  ( ( W e. A /\ C e. V ) -> ( E ` ndx ) e. _V )
40 fvsng 
 |-  ( ( ( E ` ndx ) e. _V /\ C e. V ) -> ( { <. ( E ` ndx ) , C >. } ` ( E ` ndx ) ) = C )
41 39 40 sylancom 
 |-  ( ( W e. A /\ C e. V ) -> ( { <. ( E ` ndx ) , C >. } ` ( E ` ndx ) ) = C )
42 38 41 eqtrd 
 |-  ( ( W e. A /\ C e. V ) -> ( ( ( W |` ( _V \ { ( E ` ndx ) } ) ) u. { <. ( E ` ndx ) , C >. } ) ` ( E ` ndx ) ) = C )
43 3 9 42 3eqtrrd 
 |-  ( ( W e. A /\ C e. V ) -> C = ( E ` ( W sSet <. ( E ` ndx ) , C >. ) ) )