Metamath Proof Explorer

Theorem setsres

Description: The structure replacement function does not affect the value of S away from A . (Contributed by Mario Carneiro, 1-Dec-2014) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Assertion setsres 
|- ( S e. V -> ( ( S sSet <. A , B >. ) |` ( _V \ { A } ) ) = ( S |` ( _V \ { A } ) ) )

Proof

Step Hyp Ref Expression
1 opex 
 |-  <. A , B >. e. _V
2 setsvalg 
 |-  ( ( S e. V /\ <. A , B >. e. _V ) -> ( S sSet <. A , B >. ) = ( ( S |` ( _V \ dom { <. A , B >. } ) ) u. { <. A , B >. } ) )
3 1 2 mpan2 
 |-  ( S e. V -> ( S sSet <. A , B >. ) = ( ( S |` ( _V \ dom { <. A , B >. } ) ) u. { <. A , B >. } ) )
4 3 reseq1d 
 |-  ( S e. V -> ( ( S sSet <. A , B >. ) |` ( _V \ { A } ) ) = ( ( ( S |` ( _V \ dom { <. A , B >. } ) ) u. { <. A , B >. } ) |` ( _V \ { A } ) ) )
5 resundir 
 |-  ( ( ( S |` ( _V \ dom { <. A , B >. } ) ) u. { <. A , B >. } ) |` ( _V \ { A } ) ) = ( ( ( S |` ( _V \ dom { <. A , B >. } ) ) |` ( _V \ { A } ) ) u. ( { <. A , B >. } |` ( _V \ { A } ) ) )
6 dmsnopss 
 |-  dom { <. A , B >. } C_ { A }
7 sscon 
 |-  ( dom { <. A , B >. } C_ { A } -> ( _V \ { A } ) C_ ( _V \ dom { <. A , B >. } ) )
8 6 7 ax-mp 
 |-  ( _V \ { A } ) C_ ( _V \ dom { <. A , B >. } )
9 resabs1 
 |-  ( ( _V \ { A } ) C_ ( _V \ dom { <. A , B >. } ) -> ( ( S |` ( _V \ dom { <. A , B >. } ) ) |` ( _V \ { A } ) ) = ( S |` ( _V \ { A } ) ) )
10 8 9 ax-mp 
 |-  ( ( S |` ( _V \ dom { <. A , B >. } ) ) |` ( _V \ { A } ) ) = ( S |` ( _V \ { A } ) )
11 dmres 
 |-  dom ( { <. A , B >. } |` ( _V \ { A } ) ) = ( ( _V \ { A } ) i^i dom { <. A , B >. } )
12 disj2 
 |-  ( ( ( _V \ { A } ) i^i dom { <. A , B >. } ) = (/) <-> ( _V \ { A } ) C_ ( _V \ dom { <. A , B >. } ) )
13 8 12 mpbir 
 |-  ( ( _V \ { A } ) i^i dom { <. A , B >. } ) = (/)
14 11 13 eqtri 
 |-  dom ( { <. A , B >. } |` ( _V \ { A } ) ) = (/)
15 relres 
 |-  Rel ( { <. A , B >. } |` ( _V \ { A } ) )
16 reldm0 
 |-  ( Rel ( { <. A , B >. } |` ( _V \ { A } ) ) -> ( ( { <. A , B >. } |` ( _V \ { A } ) ) = (/) <-> dom ( { <. A , B >. } |` ( _V \ { A } ) ) = (/) ) )
17 15 16 ax-mp 
 |-  ( ( { <. A , B >. } |` ( _V \ { A } ) ) = (/) <-> dom ( { <. A , B >. } |` ( _V \ { A } ) ) = (/) )
18 14 17 mpbir 
 |-  ( { <. A , B >. } |` ( _V \ { A } ) ) = (/)
19 10 18 uneq12i 
 |-  ( ( ( S |` ( _V \ dom { <. A , B >. } ) ) |` ( _V \ { A } ) ) u. ( { <. A , B >. } |` ( _V \ { A } ) ) ) = ( ( S |` ( _V \ { A } ) ) u. (/) )
20 un0 
 |-  ( ( S |` ( _V \ { A } ) ) u. (/) ) = ( S |` ( _V \ { A } ) )
21 19 20 eqtri 
 |-  ( ( ( S |` ( _V \ dom { <. A , B >. } ) ) |` ( _V \ { A } ) ) u. ( { <. A , B >. } |` ( _V \ { A } ) ) ) = ( S |` ( _V \ { A } ) )
22 5 21 eqtri 
 |-  ( ( ( S |` ( _V \ dom { <. A , B >. } ) ) u. { <. A , B >. } ) |` ( _V \ { A } ) ) = ( S |` ( _V \ { A } ) )
23 4 22 eqtrdi 
 |-  ( S e. V -> ( ( S sSet <. A , B >. ) |` ( _V \ { A } ) ) = ( S |` ( _V \ { A } ) ) )