df2ndres

Description: Definition for a restriction of the 2nd (second member of an ordered pair) function. (Contributed by Thierry Arnoux, 27-Sep-2017)

		Ref	Expression
	Assertion	df2ndres	$⊢ {2^{nd} ↾}_{(A \times B)} = (x \in A, y \in B ⟼ y)$

Step	Hyp	Ref	Expression
1		df2nd2	$⊢ \{⟨⟨x, y⟩, z⟩ \| z = y\} = {2^{nd} ↾}_{(V \times V)}$
2	1	reseq1i	$⊢ {\{⟨⟨x, y⟩, z⟩ \| z = y\} ↾}_{(A \times B)} = {({2^{nd} ↾}_{(V \times V)}) ↾}_{(A \times B)}$
3		resoprab	$⊢ {\{⟨⟨x, y⟩, z⟩ \| z = y\} ↾}_{(A \times B)} = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = y)\}$
4		resres	$⊢ {({2^{nd} ↾}_{(V \times V)}) ↾}_{(A \times B)} = {2^{nd} ↾}_{((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	$⊢ {2^{nd} ↾}_{((V \times V) \cap (A \times B))} = {2^{nd} ↾}_{(A \times B)}$
11	4 10	eqtri	$⊢ {({2^{nd} ↾}_{(V \times V)}) ↾}_{(A \times B)} = {2^{nd} ↾}_{(A \times B)}$
12	2 3 11	3eqtr3ri	$⊢ {2^{nd} ↾}_{(A \times B)} = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = y)\}$
13		df-mpo	$⊢ (x \in A, y \in B ⟼ y) = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = y)\}$
14	12 13	eqtr4i	$⊢ {2^{nd} ↾}_{(A \times B)} = (x \in A, y \in B ⟼ y)$

Metamath Proof Explorer