Theorem df1st2

Description: An alternate possible definition of the 1st function. (Contributed by NM, 14-Oct-2004) (Revised by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Assertion	df1st2	$$⊢\left\{⟨⟨x,y⟩,z⟩|z=x\right\}={1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}$$

Proof

Step	Hyp	Ref	Expression
1		fo1st	$$⊢1^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$$
2		fofn	$$⊢1^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\to 1^{st}Fn\mathrm{V}$$
3	1 2	ax-mp	$$⊢1^{st}Fn\mathrm{V}$$
4		dffn5	$$⊢1^{st}Fn\mathrm{V}\leftrightarrow 1^{st}=\left(w\in \mathrm{V}⟼1^{st}\left(w\right)\right)$$
5	3 4	mpbi	$$⊢1^{st}=\left(w\in \mathrm{V}⟼1^{st}\left(w\right)\right)$$
6		mptv	$$⊢\left(w\in \mathrm{V}⟼1^{st}\left(w\right)\right)=\left\{⟨w,z⟩|z=1^{st}\left(w\right)\right\}$$
7	5 6	eqtri	$$⊢1^{st}=\left\{⟨w,z⟩|z=1^{st}\left(w\right)\right\}$$
8	7	reseq1i	$$⊢{1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}={\left\{⟨w,z⟩|z=1^{st}\left(w\right)\right\}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}$$
9		resopab	$$⊢{\left\{⟨w,z⟩|z=1^{st}\left(w\right)\right\}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}=\left\{⟨w,z⟩|\left(w\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge z=1^{st}\left(w\right)\right)\right\}$$
10		vex	$$⊢x\in \mathrm{V}$$
11		vex	$$⊢y\in \mathrm{V}$$
12	10 11	op1std	$$⊢w=⟨x,y⟩\to 1^{st}\left(w\right)=x$$
13	12	eqeq2d	$$⊢w=⟨x,y⟩\to \left(z=1^{st}\left(w\right)\leftrightarrow z=x\right)$$
14	13	dfoprab3	$$⊢\left\{⟨w,z⟩|\left(w\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge z=1^{st}\left(w\right)\right)\right\}=\left\{⟨⟨x,y⟩,z⟩|z=x\right\}$$
15	8 9 14	3eqtrri	$$⊢\left\{⟨⟨x,y⟩,z⟩|z=x\right\}={1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}$$