Theorem df2ndres

Description: Definition for a restriction of the 2nd (second member of an ordered pair) function. (Contributed by Thierry Arnoux, 27-Sep-2017)

	Ref	Expression
Assertion	df2ndres	$$⊢{2^{nd}\upharpoonright }_{\left(A\times B\right)}=\left(x\in A,y\in B⟼y\right)$$

Proof

Step	Hyp	Ref	Expression
1		df2nd2	$$⊢\left\{⟨⟨x,y⟩,z⟩|z=y\right\}={2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}$$
2	1	reseq1i	$$⊢{\left\{⟨⟨x,y⟩,z⟩|z=y\right\}\upharpoonright }_{\left(A\times B\right)}={\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\upharpoonright }_{\left(A\times B\right)}$$
3		resoprab	$$⊢{\left\{⟨⟨x,y⟩,z⟩|z=y\right\}\upharpoonright }_{\left(A\times B\right)}=\left\{⟨⟨x,y⟩,z⟩|\left(\left(x\in A\wedge y\in B\right)\wedge z=y\right)\right\}$$
4		resres	$$⊢{\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\upharpoonright }_{\left(A\times B\right)}={2^{nd}\upharpoonright }_{\left(\left(\mathrm{V}\times \mathrm{V}\right)\cap \left(A\times B\right)\right)}$$
5		incom	$$⊢\left(A\times B\right)\cap \left(\mathrm{V}\times \mathrm{V}\right)=\left(\mathrm{V}\times \mathrm{V}\right)\cap \left(A\times B\right)$$
6		xpss	$$⊢A\times B\subseteq \mathrm{V}\times \mathrm{V}$$
7		dfss2	$$⊢A\times B\subseteq \mathrm{V}\times \mathrm{V}\leftrightarrow \left(A\times B\right)\cap \left(\mathrm{V}\times \mathrm{V}\right)=A\times B$$
8	6 7	mpbi	$$⊢\left(A\times B\right)\cap \left(\mathrm{V}\times \mathrm{V}\right)=A\times B$$
9	5 8	eqtr3i	$$⊢\left(\mathrm{V}\times \mathrm{V}\right)\cap \left(A\times B\right)=A\times B$$
10	9	reseq2i	$$⊢{2^{nd}\upharpoonright }_{\left(\left(\mathrm{V}\times \mathrm{V}\right)\cap \left(A\times B\right)\right)}={2^{nd}\upharpoonright }_{\left(A\times B\right)}$$
11	4 10	eqtri	$$⊢{\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\upharpoonright }_{\left(A\times B\right)}={2^{nd}\upharpoonright }_{\left(A\times B\right)}$$
12	2 3 11	3eqtr3ri	$$⊢{2^{nd}\upharpoonright }_{\left(A\times B\right)}=\left\{⟨⟨x,y⟩,z⟩|\left(\left(x\in A\wedge y\in B\right)\wedge z=y\right)\right\}$$
13		df-mpo	$$⊢\left(x\in A,y\in B⟼y\right)=\left\{⟨⟨x,y⟩,z⟩|\left(\left(x\in A\wedge y\in B\right)\wedge z=y\right)\right\}$$
14	12 13	eqtr4i	$$⊢{2^{nd}\upharpoonright }_{\left(A\times B\right)}=\left(x\in A,y\in B⟼y\right)$$