Metamath Proof Explorer


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 )