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	biimpi	|- ( Fun F -> F Fn dom F )
3	2	adantr	|- ( ( Fun F /\ C C_ ran F ) -> F Fn dom F )
4		sseqin2	|- ( C C_ ran F <-> ( ran F i^i C ) = C )
5	4	biimpi	|- ( C C_ ran F -> ( ran F i^i C ) = C )
6	5	eqcomd	|- ( C C_ ran F -> C = ( ran F i^i C ) )
7	6	adantl	|- ( ( Fun F /\ C C_ ran F ) -> C = ( ran F i^i C ) )
8		eqidd	|- ( ( Fun F /\ C C_ ran F ) -> ( `' F " C ) = ( `' F " C ) )
9	3 7 8	rescnvimafod	|- ( ( Fun F /\ C C_ ran F ) -> ( F |` ( `' F " C ) ) : ( `' F " C ) -onto-> C )