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

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

Metamath Proof Explorer