Theorem rescnvimafod

Description: The restriction of a function to a preimage of a class is a function onto the intersection of this class and the range of the function. (Contributed by AV, 13-Sep-2024) (Revised by AV, 29-Sep-2024)

	Ref	Expression
Hypotheses	rescnvimafod.f	|- ( ph -> F Fn A )
	rescnvimafod.e	|- ( ph -> E = ( ran F i^i B ) )
	rescnvimafod.d	|- ( ph -> D = ( `' F " B ) )
Assertion	rescnvimafod	|- ( ph -> ( F |` D ) : D -onto-> E )

Proof

Step	Hyp	Ref	Expression
1		rescnvimafod.f	|- ( ph -> F Fn A )
2		rescnvimafod.e	|- ( ph -> E = ( ran F i^i B ) )
3		rescnvimafod.d	|- ( ph -> D = ( `' F " B ) )
4		cnvimass	|- ( `' F " B ) C_ dom F
5	4	a1i	|- ( ph -> ( `' F " B ) C_ dom F )
6	1	fndmd	|- ( ph -> dom F = A )
7	6	eqcomd	|- ( ph -> A = dom F )
8	5 3 7	3sstr4d	|- ( ph -> D C_ A )
9	1 8	fnssresd	|- ( ph -> ( F |` D ) Fn D )
10		df-ima	|- ( F " D ) = ran ( F |` D )
11	3	imaeq2d	|- ( ph -> ( F " D ) = ( F " ( `' F " B ) ) )
12		fnfun	|- ( F Fn A -> Fun F )
13		funimacnv	|- ( Fun F -> ( F " ( `' F " B ) ) = ( B i^i ran F ) )
14	1 12 13	3syl	|- ( ph -> ( F " ( `' F " B ) ) = ( B i^i ran F ) )
15		incom	|- ( B i^i ran F ) = ( ran F i^i B )
16	15	a1i	|- ( ph -> ( B i^i ran F ) = ( ran F i^i B ) )
17	11 14 16	3eqtrd	|- ( ph -> ( F " D ) = ( ran F i^i B ) )
18	10 17	eqtr3id	|- ( ph -> ran ( F |` D ) = ( ran F i^i B ) )
19	18 2	eqtr4d	|- ( ph -> ran ( F |` D ) = E )
20		df-fo	|- ( ( F |` D ) : D -onto-> E <-> ( ( F |` D ) Fn D /\ ran ( F |` D ) = E ) )
21	9 19 20	sylanbrc	|- ( ph -> ( F |` D ) : D -onto-> E )