Metamath Proof Explorer


Theorem fo2ndf

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

Ref Expression
Assertion fo2ndf
|- ( F : A --> B -> ( 2nd |` F ) : F -onto-> ran F )

Proof

Step Hyp Ref Expression
1 ffrn
 |-  ( F : A --> B -> F : A --> ran F )
2 f2ndf
 |-  ( F : A --> ran F -> ( 2nd |` F ) : F --> ran F )
3 1 2 syl
 |-  ( F : A --> B -> ( 2nd |` F ) : F --> ran F )
4 ffn
 |-  ( F : A --> B -> F Fn A )
5 dffn3
 |-  ( F Fn A <-> F : A --> ran F )
6 5 2 sylbi
 |-  ( F Fn A -> ( 2nd |` F ) : F --> ran F )
7 4 6 syl
 |-  ( F : A --> B -> ( 2nd |` F ) : F --> ran F )
8 7 frnd
 |-  ( F : A --> B -> ran ( 2nd |` F ) C_ ran F )
9 elrn2g
 |-  ( y e. ran F -> ( y e. ran F <-> E. x <. x , y >. e. F ) )
10 9 ibi
 |-  ( y e. ran F -> E. x <. x , y >. e. F )
11 fvres
 |-  ( <. x , y >. e. F -> ( ( 2nd |` F ) ` <. x , y >. ) = ( 2nd ` <. x , y >. ) )
12 11 adantl
 |-  ( ( F : A --> B /\ <. x , y >. e. F ) -> ( ( 2nd |` F ) ` <. x , y >. ) = ( 2nd ` <. x , y >. ) )
13 vex
 |-  x e. _V
14 vex
 |-  y e. _V
15 13 14 op2nd
 |-  ( 2nd ` <. x , y >. ) = y
16 12 15 eqtr2di
 |-  ( ( F : A --> B /\ <. x , y >. e. F ) -> y = ( ( 2nd |` F ) ` <. x , y >. ) )
17 f2ndf
 |-  ( F : A --> B -> ( 2nd |` F ) : F --> B )
18 17 ffnd
 |-  ( F : A --> B -> ( 2nd |` F ) Fn F )
19 fnfvelrn
 |-  ( ( ( 2nd |` F ) Fn F /\ <. x , y >. e. F ) -> ( ( 2nd |` F ) ` <. x , y >. ) e. ran ( 2nd |` F ) )
20 18 19 sylan
 |-  ( ( F : A --> B /\ <. x , y >. e. F ) -> ( ( 2nd |` F ) ` <. x , y >. ) e. ran ( 2nd |` F ) )
21 16 20 eqeltrd
 |-  ( ( F : A --> B /\ <. x , y >. e. F ) -> y e. ran ( 2nd |` F ) )
22 21 ex
 |-  ( F : A --> B -> ( <. x , y >. e. F -> y e. ran ( 2nd |` F ) ) )
23 22 exlimdv
 |-  ( F : A --> B -> ( E. x <. x , y >. e. F -> y e. ran ( 2nd |` F ) ) )
24 10 23 syl5
 |-  ( F : A --> B -> ( y e. ran F -> y e. ran ( 2nd |` F ) ) )
25 24 ssrdv
 |-  ( F : A --> B -> ran F C_ ran ( 2nd |` F ) )
26 8 25 eqssd
 |-  ( F : A --> B -> ran ( 2nd |` F ) = ran F )
27 dffo2
 |-  ( ( 2nd |` F ) : F -onto-> ran F <-> ( ( 2nd |` F ) : F --> ran F /\ ran ( 2nd |` F ) = ran F ) )
28 3 26 27 sylanbrc
 |-  ( F : A --> B -> ( 2nd |` F ) : F -onto-> ran F )