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 -> ( 2nd |` F ) : F --> B )

Proof

Step	Hyp	Ref	Expression
1		f2ndres	|- ( 2nd |` ( A X. B ) ) : ( A X. B ) --> B
2		fssxp	|- ( F : A --> B -> F C_ ( A X. B ) )
3		fssres	|- ( ( ( 2nd |` ( A X. B ) ) : ( A X. B ) --> B /\ F C_ ( A X. B ) ) -> ( ( 2nd |` ( A X. B ) ) |` F ) : F --> B )
4	1 2 3	sylancr	|- ( F : A --> B -> ( ( 2nd |` ( A X. B ) ) |` F ) : F --> B )
5	2	resabs1d	|- ( F : A --> B -> ( ( 2nd |` ( A X. B ) ) |` F ) = ( 2nd |` F ) )
6	5	eqcomd	|- ( F : A --> B -> ( 2nd |` F ) = ( ( 2nd |` ( A X. B ) ) |` F ) )
7	6	feq1d	|- ( F : A --> B -> ( ( 2nd |` F ) : F --> B <-> ( ( 2nd |` ( A X. B ) ) |` F ) : F --> B ) )
8	4 7	mpbird	|- ( F : A --> B -> ( 2nd |` F ) : F --> B )