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

Metamath Proof Explorer

Theorem fores

Description: Restriction of an onto function. (Contributed by NM, 4-Mar-1997)

Ref Expression
Assertion fores 
|- ( ( Fun F /\ A C_ dom F ) -> ( F |` A ) : A -onto-> ( F " A ) )

Proof

Step Hyp Ref Expression
1 funres 
 |-  ( Fun F -> Fun ( F |` A ) )
2 1 anim1i 
 |-  ( ( Fun F /\ A C_ dom F ) -> ( Fun ( F |` A ) /\ A C_ dom F ) )
3 df-fn 
 |-  ( ( F |` A ) Fn A <-> ( Fun ( F |` A ) /\ dom ( F |` A ) = A ) )
4 df-ima 
 |-  ( F " A ) = ran ( F |` A )
5 4 eqcomi 
 |-  ran ( F |` A ) = ( F " A )
6 df-fo 
 |-  ( ( F |` A ) : A -onto-> ( F " A ) <-> ( ( F |` A ) Fn A /\ ran ( F |` A ) = ( F " A ) ) )
7 5 6 mpbiran2 
 |-  ( ( F |` A ) : A -onto-> ( F " A ) <-> ( F |` A ) Fn A )
8 ssdmres 
 |-  ( A C_ dom F <-> dom ( F |` A ) = A )
9 8 anbi2i 
 |-  ( ( Fun ( F |` A ) /\ A C_ dom F ) <-> ( Fun ( F |` A ) /\ dom ( F |` A ) = A ) )
10 3 7 9 3bitr4i 
 |-  ( ( F |` A ) : A -onto-> ( F " A ) <-> ( Fun ( F |` A ) /\ A C_ dom F ) )
11 2 10 sylibr 
 |-  ( ( Fun F /\ A C_ dom F ) -> ( F |` A ) : A -onto-> ( F " A ) )