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} ↾}_{(A \times B)} = (x \in A, y \in B ⟼ x)$

Step	Hyp	Ref	Expression
1		df1st2	$⊢ \{⟨⟨x, y⟩, z⟩ \| z = x\} = {1^{st} ↾}_{(V \times V)}$
2	1	reseq1i	$⊢ {\{⟨⟨x, y⟩, z⟩ \| z = x\} ↾}_{(A \times B)} = {({1^{st} ↾}_{(V \times V)}) ↾}_{(A \times B)}$
3		resoprab	$⊢ {\{⟨⟨x, y⟩, z⟩ \| z = x\} ↾}_{(A \times B)} = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = x)\}$
4		resres	$⊢ {({1^{st} ↾}_{(V \times V)}) ↾}_{(A \times B)} = {1^{st} ↾}_{((V \times V) \cap (A \times B))}$
5		incom	$⊢ (A \times B) \cap (V \times V) = (V \times V) \cap (A \times B)$
6		xpss	$⊢ A \times B \subseteq V \times V$
7		df-ss	$⊢ A \times B \subseteq V \times V \leftrightarrow (A \times B) \cap (V \times V) = A \times B$
8	6 7	mpbi	$⊢ (A \times B) \cap (V \times V) = A \times B$
9	5 8	eqtr3i	$⊢ (V \times V) \cap (A \times B) = A \times B$
10	9	reseq2i	$⊢ {1^{st} ↾}_{((V \times V) \cap (A \times B))} = {1^{st} ↾}_{(A \times B)}$
11	4 10	eqtri	$⊢ {({1^{st} ↾}_{(V \times V)}) ↾}_{(A \times B)} = {1^{st} ↾}_{(A \times B)}$
12	2 3 11	3eqtr3ri	$⊢ {1^{st} ↾}_{(A \times B)} = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = x)\}$
13		df-mpo	$⊢ (x \in A, y \in B ⟼ x) = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = x)\}$
14	12 13	eqtr4i	$⊢ {1^{st} ↾}_{(A \times B)} = (x \in A, y \in B ⟼ x)$

Metamath Proof Explorer