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	bilanri	$$⊢\left(y\in A\wedge z\in B\right)\to \bigcup \mathrm{ran}\left\{⟨y,z⟩\right\}\in B$$
6	5	rgen2	$$⊢\forall y\in A\forall z\in B\bigcup \mathrm{ran}\left\{⟨y,z⟩\right\}\in B$$
7		sneq	$$⊢x=⟨y,z⟩\to \left\{x\right\}=\left\{⟨y,z⟩\right\}$$
8	7	rneqd	$$⊢x=⟨y,z⟩\to \mathrm{ran}\left\{x\right\}=\mathrm{ran}\left\{⟨y,z⟩\right\}$$
9	8	unieqd	$$⊢x=⟨y,z⟩\to \bigcup \mathrm{ran}\left\{x\right\}=\bigcup \mathrm{ran}\left\{⟨y,z⟩\right\}$$
10	9	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)$$
11	10	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$$
12	6 11	mpbir	$$⊢\forall x\in \left(A\times B\right)\bigcup \mathrm{ran}\left\{x\right\}\in B$$
13		df-2nd	$$⊢2^{nd}=\left(x\in \mathrm{V}⟼\bigcup \mathrm{ran}\left\{x\right\}\right)$$
14	13	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)}$$
15		ssv	$$⊢A\times B\subseteq \mathrm{V}$$
16		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)$$
17	15 16	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)$$
18	14 17	eqtri	$$⊢{2^{nd}\upharpoonright }_{\left(A\times B\right)}=\left(x\in \left(A\times B\right)⟼\bigcup \mathrm{ran}\left\{x\right\}\right)$$
19	18	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$$
20	12 19	mpbi	$$⊢\left({2^{nd}\upharpoonright }_{\left(A\times B\right)}\right):A\times B⟶B$$