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 incom 
 |-  ( ( _V \ { ( E ` ndx ) } ) i^i { ( E ` ndx ) } ) = ( { ( E ` ndx ) } i^i ( _V \ { ( E ` ndx ) } ) )
16 disjdif 
 |-  ( { ( E ` ndx ) } i^i ( _V \ { ( E ` ndx ) } ) ) = (/)
17 15 16 eqtri 
 |-  ( ( _V \ { ( E ` ndx ) } ) i^i { ( E ` ndx ) } ) = (/)
18 17 reseq2i 
 |-  ( W |` ( ( _V \ { ( E ` ndx ) } ) i^i { ( E ` ndx ) } ) ) = ( W |` (/) )
19 res0 
 |-  ( W |` (/) ) = (/)
20 18 19 eqtri 
 |-  ( W |` ( ( _V \ { ( E ` ndx ) } ) i^i { ( E ` ndx ) } ) ) = (/)
21 14 20 eqtri 
 |-  ( ( W |` ( _V \ { ( E ` ndx ) } ) ) |` { ( E ` ndx ) } ) = (/)
22 21 a1i 
 |-  ( ( W e. A /\ C e. V ) -> ( ( W |` ( _V \ { ( E ` ndx ) } ) ) |` { ( E ` ndx ) } ) = (/) )
23 elex 
 |-  ( C e. V -> C e. _V )
24 23 adantl 
 |-  ( ( W e. A /\ C e. V ) -> C e. _V )
25 opelxpi 
 |-  ( ( ( E ` ndx ) e. _V /\ C e. _V ) -> <. ( E ` ndx ) , C >. e. ( _V X. _V ) )
26 10 24 25 sylancr 
 |-  ( ( W e. A /\ C e. V ) -> <. ( E ` ndx ) , C >. e. ( _V X. _V ) )
27 opex 
 |-  <. ( E ` ndx ) , C >. e. _V
28 27 relsn 
 |-  ( Rel { <. ( E ` ndx ) , C >. } <-> <. ( E ` ndx ) , C >. e. ( _V X. _V ) )
29 26 28 sylibr 
 |-  ( ( W e. A /\ C e. V ) -> Rel { <. ( E ` ndx ) , C >. } )
30 dmsnopss 
 |-  dom { <. ( E ` ndx ) , C >. } C_ { ( E ` ndx ) }
31 relssres 
 |-  ( ( Rel { <. ( E ` ndx ) , C >. } /\ dom { <. ( E ` ndx ) , C >. } C_ { ( E ` ndx ) } ) -> ( { <. ( E ` ndx ) , C >. } |` { ( E ` ndx ) } ) = { <. ( E ` ndx ) , C >. } )
32 29 30 31 sylancl 
 |-  ( ( W e. A /\ C e. V ) -> ( { <. ( E ` ndx ) , C >. } |` { ( E ` ndx ) } ) = { <. ( E ` ndx ) , C >. } )
33 22 32 uneq12d 
 |-  ( ( W e. A /\ C e. V ) -> ( ( ( W |` ( _V \ { ( E ` ndx ) } ) ) |` { ( E ` ndx ) } ) u. ( { <. ( E ` ndx ) , C >. } |` { ( E ` ndx ) } ) ) = ( (/) u. { <. ( E ` ndx ) , C >. } ) )
34 resundir 
 |-  ( ( ( W |` ( _V \ { ( E ` ndx ) } ) ) u. { <. ( E ` ndx ) , C >. } ) |` { ( E ` ndx ) } ) = ( ( ( W |` ( _V \ { ( E ` ndx ) } ) ) |` { ( E ` ndx ) } ) u. ( { <. ( E ` ndx ) , C >. } |` { ( E ` ndx ) } ) )
35 un0 
 |-  ( { <. ( E ` ndx ) , C >. } u. (/) ) = { <. ( E ` ndx ) , C >. }
36 uncom 
 |-  ( { <. ( E ` ndx ) , C >. } u. (/) ) = ( (/) u. { <. ( E ` ndx ) , C >. } )
37 35 36 eqtr3i 
 |-  { <. ( E ` ndx ) , C >. } = ( (/) u. { <. ( E ` ndx ) , C >. } )
38 33 34 37 3eqtr4g 
 |-  ( ( W e. A /\ C e. V ) -> ( ( ( W |` ( _V \ { ( E ` ndx ) } ) ) u. { <. ( E ` ndx ) , C >. } ) |` { ( E ` ndx ) } ) = { <. ( E ` ndx ) , C >. } )
39 38 fveq1d 
 |-  ( ( W e. A /\ C e. V ) -> ( ( ( ( W |` ( _V \ { ( E ` ndx ) } ) ) u. { <. ( E ` ndx ) , C >. } ) |` { ( E ` ndx ) } ) ` ( E ` ndx ) ) = ( { <. ( E ` ndx ) , C >. } ` ( E ` ndx ) ) )
40 13 39 syl5eqr 
 |-  ( ( W e. A /\ C e. V ) -> ( ( ( W |` ( _V \ { ( E ` ndx ) } ) ) u. { <. ( E ` ndx ) , C >. } ) ` ( E ` ndx ) ) = ( { <. ( E ` ndx ) , C >. } ` ( E ` ndx ) ) )
41 10 a1i 
 |-  ( ( W e. A /\ C e. V ) -> ( E ` ndx ) e. _V )
42 fvsng 
 |-  ( ( ( E ` ndx ) e. _V /\ C e. V ) -> ( { <. ( E ` ndx ) , C >. } ` ( E ` ndx ) ) = C )
43 41 42 sylancom 
 |-  ( ( W e. A /\ C e. V ) -> ( { <. ( E ` ndx ) , C >. } ` ( E ` ndx ) ) = C )
44 40 43 eqtrd 
 |-  ( ( W e. A /\ C e. V ) -> ( ( ( W |` ( _V \ { ( E ` ndx ) } ) ) u. { <. ( E ` ndx ) , C >. } ) ` ( E ` ndx ) ) = C )
45 3 9 44 3eqtrrd 
 |-  ( ( W e. A /\ C e. V ) -> C = ( E ` ( W sSet <. ( E ` ndx ) , C >. ) ) )