Theorem df1stres

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

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

Proof

Step	Hyp	Ref	Expression
1		df1st2	$$⊢\left\{⟨⟨x,y⟩,z⟩|z=x\right\}={1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}$$
2	1	reseq1i	$$⊢{\left\{⟨⟨x,y⟩,z⟩|z=x\right\}\upharpoonright }_{\left(A\times B\right)}={\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\upharpoonright }_{\left(A\times B\right)}$$
3		resoprab	$$⊢{\left\{⟨⟨x,y⟩,z⟩|z=x\right\}\upharpoonright }_{\left(A\times B\right)}=\left\{⟨⟨x,y⟩,z⟩|\left(\left(x\in A\wedge y\in B\right)\wedge z=x\right)\right\}$$
4		resres	$$⊢{\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\upharpoonright }_{\left(A\times B\right)}={1^{st}\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	$$⊢{1^{st}\upharpoonright }_{\left(\left(\mathrm{V}\times \mathrm{V}\right)\cap \left(A\times B\right)\right)}={1^{st}\upharpoonright }_{\left(A\times B\right)}$$
11	4 10	eqtri	$$⊢{\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\upharpoonright }_{\left(A\times B\right)}={1^{st}\upharpoonright }_{\left(A\times B\right)}$$
12	2 3 11	3eqtr3ri	$$⊢{1^{st}\upharpoonright }_{\left(A\times B\right)}=\left\{⟨⟨x,y⟩,z⟩|\left(\left(x\in A\wedge y\in B\right)\wedge z=x\right)\right\}$$
13		df-mpo	$$⊢\left(x\in A,y\in B⟼x\right)=\left\{⟨⟨x,y⟩,z⟩|\left(\left(x\in A\wedge y\in B\right)\wedge z=x\right)\right\}$$
14	12 13	eqtr4i	$$⊢{1^{st}\upharpoonright }_{\left(A\times B\right)}=\left(x\in A,y\in B⟼x\right)$$