Theorem df2nd2

Description: An alternate possible definition of the 2nd function. (Contributed by NM, 10-Aug-2006) (Revised by Mario Carneiro, 31-Aug-2015)

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

Proof

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