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 ) )