This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )