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 )