Theorem fimadmfoALT

Description: Alternate proof of fimadmfo , based on fores . A function is a function onto the image of its domain. (Contributed by AV, 1-Dec-2022) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	fimadmfoALT	|- ( F : A --> B -> F : A -onto-> ( F " A ) )

Proof

Step	Hyp	Ref	Expression
1		fdm	|- ( F : A --> B -> dom F = A )
2		frel	|- ( F : A --> B -> Rel F )
3		resdm	|- ( Rel F -> ( F |` dom F ) = F )
4	3	eqcomd	|- ( Rel F -> F = ( F |` dom F ) )
5	2 4	syl	|- ( F : A --> B -> F = ( F |` dom F ) )
6		reseq2	|- ( dom F = A -> ( F |` dom F ) = ( F |` A ) )
7	5 6	sylan9eq	|- ( ( F : A --> B /\ dom F = A ) -> F = ( F |` A ) )
8	1 7	mpdan	|- ( F : A --> B -> F = ( F |` A ) )
9		ffun	|- ( F : A --> B -> Fun F )
10		eqimss2	|- ( dom F = A -> A C_ dom F )
11	1 10	syl	|- ( F : A --> B -> A C_ dom F )
12	9 11	jca	|- ( F : A --> B -> ( Fun F /\ A C_ dom F ) )
13	12	adantr	|- ( ( F : A --> B /\ F = ( F |` A ) ) -> ( Fun F /\ A C_ dom F ) )
14		fores	|- ( ( Fun F /\ A C_ dom F ) -> ( F |` A ) : A -onto-> ( F " A ) )
15	13 14	syl	|- ( ( F : A --> B /\ F = ( F |` A ) ) -> ( F |` A ) : A -onto-> ( F " A ) )
16		foeq1	|- ( F = ( F |` A ) -> ( F : A -onto-> ( F " A ) <-> ( F |` A ) : A -onto-> ( F " A ) ) )
17	16	adantl	|- ( ( F : A --> B /\ F = ( F |` A ) ) -> ( F : A -onto-> ( F " A ) <-> ( F |` A ) : A -onto-> ( F " A ) ) )
18	15 17	mpbird	|- ( ( F : A --> B /\ F = ( F |` A ) ) -> F : A -onto-> ( F " A ) )
19	8 18	mpdan	|- ( F : A --> B -> F : A -onto-> ( F " A ) )