This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem residpr

Description: Restriction of the identity to a pair. (Contributed by AV, 11-Dec-2018)

Ref Expression
Assertion residpr 
|- ( ( A e. V /\ B e. W ) -> ( _I |` { A , B } ) = { <. A , A >. , <. B , B >. } )

Proof

Step Hyp Ref Expression
1 df-pr 
 |-  { A , B } = ( { A } u. { B } )
2 1 reseq2i 
 |-  ( _I |` { A , B } ) = ( _I |` ( { A } u. { B } ) )
3 resundi 
 |-  ( _I |` ( { A } u. { B } ) ) = ( ( _I |` { A } ) u. ( _I |` { B } ) )
4 2 3 eqtri 
 |-  ( _I |` { A , B } ) = ( ( _I |` { A } ) u. ( _I |` { B } ) )
5 xpsng 
 |-  ( ( A e. V /\ A e. V ) -> ( { A } X. { A } ) = { <. A , A >. } )
6 5 anidms 
 |-  ( A e. V -> ( { A } X. { A } ) = { <. A , A >. } )
7 6 adantr 
 |-  ( ( A e. V /\ B e. W ) -> ( { A } X. { A } ) = { <. A , A >. } )
8 xpsng 
 |-  ( ( B e. W /\ B e. W ) -> ( { B } X. { B } ) = { <. B , B >. } )
9 8 anidms 
 |-  ( B e. W -> ( { B } X. { B } ) = { <. B , B >. } )
10 9 adantl 
 |-  ( ( A e. V /\ B e. W ) -> ( { B } X. { B } ) = { <. B , B >. } )
11 7 10 uneq12d 
 |-  ( ( A e. V /\ B e. W ) -> ( ( { A } X. { A } ) u. ( { B } X. { B } ) ) = ( { <. A , A >. } u. { <. B , B >. } ) )
12 restidsing 
 |-  ( _I |` { A } ) = ( { A } X. { A } )
13 restidsing 
 |-  ( _I |` { B } ) = ( { B } X. { B } )
14 12 13 uneq12i 
 |-  ( ( _I |` { A } ) u. ( _I |` { B } ) ) = ( ( { A } X. { A } ) u. ( { B } X. { B } ) )
15 df-pr 
 |-  { <. A , A >. , <. B , B >. } = ( { <. A , A >. } u. { <. B , B >. } )
16 11 14 15 3eqtr4g 
 |-  ( ( A e. V /\ B e. W ) -> ( ( _I |` { A } ) u. ( _I |` { B } ) ) = { <. A , A >. , <. B , B >. } )
17 4 16 eqtrid 
 |-  ( ( A e. V /\ B e. W ) -> ( _I |` { A , B } ) = { <. A , A >. , <. B , B >. } )