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	$⊢ \{⟨⟨x, y⟩, z⟩ \| z = y\} = {2^{nd} ↾}_{(V \times V)}$

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

Metamath Proof Explorer