Theorem f2ndf

Description: The 2nd (second component of an ordered pair) function restricted to a function F is a function from F into the codomain of F . (Contributed by Alexander van der Vekens, 4-Feb-2018)

	Ref	Expression
Assertion	f2ndf	$$⊢F:A⟶B\to \left({2^{nd}\upharpoonright }_F\right):F⟶B$$

Proof

Step	Hyp	Ref	Expression
1		f2ndres	$$⊢\left({2^{nd}\upharpoonright }_{\left(A\times B\right)}\right):A\times B⟶B$$
2		fssxp	$$⊢F:A⟶B\to F\subseteq A\times B$$
3		fssres	$$⊢\left(\left({2^{nd}\upharpoonright }_{\left(A\times B\right)}\right):A\times B⟶B\wedge F\subseteq A\times B\right)\to \left({\left({2^{nd}\upharpoonright }_{\left(A\times B\right)}\right)\upharpoonright }_F\right):F⟶B$$
4	1 2 3	sylancr	$$⊢F:A⟶B\to \left({\left({2^{nd}\upharpoonright }_{\left(A\times B\right)}\right)\upharpoonright }_F\right):F⟶B$$
5	2	resabs1d	$$⊢F:A⟶B\to {\left({2^{nd}\upharpoonright }_{\left(A\times B\right)}\right)\upharpoonright }_F={2^{nd}\upharpoonright }_F$$
6	5	eqcomd	$$⊢F:A⟶B\to {2^{nd}\upharpoonright }_F={\left({2^{nd}\upharpoonright }_{\left(A\times B\right)}\right)\upharpoonright }_F$$
7	6	feq1d	$$⊢F:A⟶B\to \left(\left({2^{nd}\upharpoonright }_F\right):F⟶B\leftrightarrow \left({\left({2^{nd}\upharpoonright }_{\left(A\times B\right)}\right)\upharpoonright }_F\right):F⟶B\right)$$
8	4 7	mpbird	$$⊢F:A⟶B\to \left({2^{nd}\upharpoonright }_F\right):F⟶B$$