Theorem residpr

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

	Ref	Expression
Assertion	residpr	$$⊢\left(A\in V\wedge B\in W\right)\to {\mathrm{I}\upharpoonright }_{\left\{A,B\right\}}=\left\{⟨A,A⟩,⟨B,B⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-pr	$$⊢\left\{A,B\right\}=\left\{A\right\}\cup \left\{B\right\}$$
2	1	reseq2i	$$⊢{\mathrm{I}\upharpoonright }_{\left\{A,B\right\}}={\mathrm{I}\upharpoonright }_{\left(\left\{A\right\}\cup \left\{B\right\}\right)}$$
3		resundi	$$⊢{\mathrm{I}\upharpoonright }_{\left(\left\{A\right\}\cup \left\{B\right\}\right)}=\left({\mathrm{I}\upharpoonright }_{\left\{A\right\}}\right)\cup \left({\mathrm{I}\upharpoonright }_{\left\{B\right\}}\right)$$
4	2 3	eqtri	$$⊢{\mathrm{I}\upharpoonright }_{\left\{A,B\right\}}=\left({\mathrm{I}\upharpoonright }_{\left\{A\right\}}\right)\cup \left({\mathrm{I}\upharpoonright }_{\left\{B\right\}}\right)$$
5		xpsng	$$⊢\left(A\in V\wedge A\in V\right)\to \left\{A\right\}\times \left\{A\right\}=\left\{⟨A,A⟩\right\}$$
6	5	anidms	$$⊢A\in V\to \left\{A\right\}\times \left\{A\right\}=\left\{⟨A,A⟩\right\}$$
7	6	adantr	$$⊢\left(A\in V\wedge B\in W\right)\to \left\{A\right\}\times \left\{A\right\}=\left\{⟨A,A⟩\right\}$$
8		xpsng	$$⊢\left(B\in W\wedge B\in W\right)\to \left\{B\right\}\times \left\{B\right\}=\left\{⟨B,B⟩\right\}$$
9	8	anidms	$$⊢B\in W\to \left\{B\right\}\times \left\{B\right\}=\left\{⟨B,B⟩\right\}$$
10	9	adantl	$$⊢\left(A\in V\wedge B\in W\right)\to \left\{B\right\}\times \left\{B\right\}=\left\{⟨B,B⟩\right\}$$
11	7 10	uneq12d	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\left\{A\right\}\times \left\{A\right\}\right)\cup \left(\left\{B\right\}\times \left\{B\right\}\right)=\left\{⟨A,A⟩\right\}\cup \left\{⟨B,B⟩\right\}$$
12		restidsing	$$⊢{\mathrm{I}\upharpoonright }_{\left\{A\right\}}=\left\{A\right\}\times \left\{A\right\}$$
13		restidsing	$$⊢{\mathrm{I}\upharpoonright }_{\left\{B\right\}}=\left\{B\right\}\times \left\{B\right\}$$
14	12 13	uneq12i	$$⊢\left({\mathrm{I}\upharpoonright }_{\left\{A\right\}}\right)\cup \left({\mathrm{I}\upharpoonright }_{\left\{B\right\}}\right)=\left(\left\{A\right\}\times \left\{A\right\}\right)\cup \left(\left\{B\right\}\times \left\{B\right\}\right)$$
15		df-pr	$$⊢\left\{⟨A,A⟩,⟨B,B⟩\right\}=\left\{⟨A,A⟩\right\}\cup \left\{⟨B,B⟩\right\}$$
16	11 14 15	3eqtr4g	$$⊢\left(A\in V\wedge B\in W\right)\to \left({\mathrm{I}\upharpoonright }_{\left\{A\right\}}\right)\cup \left({\mathrm{I}\upharpoonright }_{\left\{B\right\}}\right)=\left\{⟨A,A⟩,⟨B,B⟩\right\}$$
17	4 16	eqtrid	$$⊢\left(A\in V\wedge B\in W\right)\to {\mathrm{I}\upharpoonright }_{\left\{A,B\right\}}=\left\{⟨A,A⟩,⟨B,B⟩\right\}$$