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 ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 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 eqtrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( I ↾ { 𝐴 , 𝐵 } ) = { ⟨ 𝐴 , 𝐴 ⟩ , ⟨ 𝐵 , 𝐵 ⟩ } )