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	syl5eq	|- ( ( A e. V /\ B e. W ) -> ( _I |` { A , B } ) = { <. A , A >. , <. B , B >. } )