This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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