Theorem fresfo

Description: Conditions for a restriction to be an onto function. Part of fresf1o . (Contributed by AV, 29-Sep-2024)

	Ref	Expression
Assertion	fresfo	|- ( ( Fun F /\ C C_ ran F ) -> ( F |` ( `' F " C ) ) : ( `' F " C ) -onto-> C )

Proof

Step	Hyp	Ref	Expression
1		funfn	|- ( Fun F <-> F Fn dom F )
2	1	birani	|- ( ( Fun F /\ C C_ ran F ) -> F Fn dom F )
3		sseqin2	|- ( C C_ ran F <-> ( ran F i^i C ) = C )
4	3	biimpi	|- ( C C_ ran F -> ( ran F i^i C ) = C )
5	4	eqcomd	|- ( C C_ ran F -> C = ( ran F i^i C ) )
6	5	adantl	|- ( ( Fun F /\ C C_ ran F ) -> C = ( ran F i^i C ) )
7		eqidd	|- ( ( Fun F /\ C C_ ran F ) -> ( `' F " C ) = ( `' F " C ) )
8	2 6 7	rescnvimafod	|- ( ( Fun F /\ C C_ ran F ) -> ( F |` ( `' F " C ) ) : ( `' F " C ) -onto-> C )