Theorem f2ndres

Description: Mapping of a restriction of the 2nd (second member of an ordered pair) function. (Contributed by NM, 7-Aug-2006) (Revised by Mario Carneiro, 8-Sep-2013)

	Ref	Expression
Assertion	f2ndres	$$⊢\left({2^{nd}\upharpoonright }_{\left(A\times B\right)}\right):A\times B⟶B$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢y\in \mathrm{V}$$
2		vex	$$⊢z\in \mathrm{V}$$
3	1 2	op2nda	$$⊢\bigcup \mathrm{ran}\left\{⟨y,z⟩\right\}=z$$
4	3	eleq1i	$$⊢\bigcup \mathrm{ran}\left\{⟨y,z⟩\right\}\in B\leftrightarrow z\in B$$
5	4	biimpri	$$⊢z\in B\to \bigcup \mathrm{ran}\left\{⟨y,z⟩\right\}\in B$$
6	5	adantl	$$⊢\left(y\in A\wedge z\in B\right)\to \bigcup \mathrm{ran}\left\{⟨y,z⟩\right\}\in B$$
7	6	rgen2	$$⊢\forall y\in A\forall z\in B\bigcup \mathrm{ran}\left\{⟨y,z⟩\right\}\in B$$
8		sneq	$$⊢x=⟨y,z⟩\to \left\{x\right\}=\left\{⟨y,z⟩\right\}$$
9	8	rneqd	$$⊢x=⟨y,z⟩\to \mathrm{ran}\left\{x\right\}=\mathrm{ran}\left\{⟨y,z⟩\right\}$$
10	9	unieqd	$$⊢x=⟨y,z⟩\to \bigcup \mathrm{ran}\left\{x\right\}=\bigcup \mathrm{ran}\left\{⟨y,z⟩\right\}$$
11	10	eleq1d	$$⊢x=⟨y,z⟩\to \left(\bigcup \mathrm{ran}\left\{x\right\}\in B\leftrightarrow \bigcup \mathrm{ran}\left\{⟨y,z⟩\right\}\in B\right)$$
12	11	ralxp	$$⊢\forall x\in \left(A\times B\right)\bigcup \mathrm{ran}\left\{x\right\}\in B\leftrightarrow \forall y\in A\forall z\in B\bigcup \mathrm{ran}\left\{⟨y,z⟩\right\}\in B$$
13	7 12	mpbir	$$⊢\forall x\in \left(A\times B\right)\bigcup \mathrm{ran}\left\{x\right\}\in B$$
14		df-2nd	$$⊢2^{nd}=\left(x\in \mathrm{V}⟼\bigcup \mathrm{ran}\left\{x\right\}\right)$$
15	14	reseq1i	$$⊢{2^{nd}\upharpoonright }_{\left(A\times B\right)}={\left(x\in \mathrm{V}⟼\bigcup \mathrm{ran}\left\{x\right\}\right)\upharpoonright }_{\left(A\times B\right)}$$
16		ssv	$$⊢A\times B\subseteq \mathrm{V}$$
17		resmpt	$$⊢A\times B\subseteq \mathrm{V}\to {\left(x\in \mathrm{V}⟼\bigcup \mathrm{ran}\left\{x\right\}\right)\upharpoonright }_{\left(A\times B\right)}=\left(x\in \left(A\times B\right)⟼\bigcup \mathrm{ran}\left\{x\right\}\right)$$
18	16 17	ax-mp	$$⊢{\left(x\in \mathrm{V}⟼\bigcup \mathrm{ran}\left\{x\right\}\right)\upharpoonright }_{\left(A\times B\right)}=\left(x\in \left(A\times B\right)⟼\bigcup \mathrm{ran}\left\{x\right\}\right)$$
19	15 18	eqtri	$$⊢{2^{nd}\upharpoonright }_{\left(A\times B\right)}=\left(x\in \left(A\times B\right)⟼\bigcup \mathrm{ran}\left\{x\right\}\right)$$
20	19	fmpt	$$⊢\forall x\in \left(A\times B\right)\bigcup \mathrm{ran}\left\{x\right\}\in B\leftrightarrow \left({2^{nd}\upharpoonright }_{\left(A\times B\right)}\right):A\times B⟶B$$
21	13 20	mpbi	$$⊢\left({2^{nd}\upharpoonright }_{\left(A\times B\right)}\right):A\times B⟶B$$