Theorem residpr

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

	Ref	Expression
Assertion	residpr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( I ↾ { 𝐴 , 𝐵 } ) = { ⟨ 𝐴 , 𝐴 ⟩ , ⟨ 𝐵 , 𝐵 ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		df-pr	⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } )
2	1	reseq2i	⊢ ( I ↾ { 𝐴 , 𝐵 } ) = ( I ↾ ( { 𝐴 } ∪ { 𝐵 } ) )
3		resundi	⊢ ( I ↾ ( { 𝐴 } ∪ { 𝐵 } ) ) = ( ( I ↾ { 𝐴 } ) ∪ ( I ↾ { 𝐵 } ) )
4	2 3	eqtri	⊢ ( I ↾ { 𝐴 , 𝐵 } ) = ( ( I ↾ { 𝐴 } ) ∪ ( I ↾ { 𝐵 } ) )
5		xpsng	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → ( { 𝐴 } × { 𝐴 } ) = { ⟨ 𝐴 , 𝐴 ⟩ } )
6	5	anidms	⊢ ( 𝐴 ∈ 𝑉 → ( { 𝐴 } × { 𝐴 } ) = { ⟨ 𝐴 , 𝐴 ⟩ } )
7	6	adantr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { 𝐴 } × { 𝐴 } ) = { ⟨ 𝐴 , 𝐴 ⟩ } )
8		xpsng	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → ( { 𝐵 } × { 𝐵 } ) = { ⟨ 𝐵 , 𝐵 ⟩ } )
9	8	anidms	⊢ ( 𝐵 ∈ 𝑊 → ( { 𝐵 } × { 𝐵 } ) = { ⟨ 𝐵 , 𝐵 ⟩ } )
10	9	adantl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { 𝐵 } × { 𝐵 } ) = { ⟨ 𝐵 , 𝐵 ⟩ } )
11	7 10	uneq12d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( { 𝐴 } × { 𝐴 } ) ∪ ( { 𝐵 } × { 𝐵 } ) ) = ( { ⟨ 𝐴 , 𝐴 ⟩ } ∪ { ⟨ 𝐵 , 𝐵 ⟩ } ) )
12		restidsing	⊢ ( I ↾ { 𝐴 } ) = ( { 𝐴 } × { 𝐴 } )
13		restidsing	⊢ ( I ↾ { 𝐵 } ) = ( { 𝐵 } × { 𝐵 } )
14	12 13	uneq12i	⊢ ( ( I ↾ { 𝐴 } ) ∪ ( I ↾ { 𝐵 } ) ) = ( ( { 𝐴 } × { 𝐴 } ) ∪ ( { 𝐵 } × { 𝐵 } ) )
15		df-pr	⊢ { ⟨ 𝐴 , 𝐴 ⟩ , ⟨ 𝐵 , 𝐵 ⟩ } = ( { ⟨ 𝐴 , 𝐴 ⟩ } ∪ { ⟨ 𝐵 , 𝐵 ⟩ } )
16	11 14 15	3eqtr4g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( I ↾ { 𝐴 } ) ∪ ( I ↾ { 𝐵 } ) ) = { ⟨ 𝐴 , 𝐴 ⟩ , ⟨ 𝐵 , 𝐵 ⟩ } )
17	4 16	syl5eq	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( I ↾ { 𝐴 , 𝐵 } ) = { ⟨ 𝐴 , 𝐴 ⟩ , ⟨ 𝐵 , 𝐵 ⟩ } )