Metamath Proof Explorer

Theorem fimadmfo

Description: A function is a function onto the image of its domain. (Contributed by AV, 1-Dec-2022)

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

Proof

Step Hyp Ref Expression
1 fdm 
 |-  ( F : A --> B -> dom F = A )
2 ffn 
 |-  ( F : A --> B -> F Fn A )
3 2 adantr 
 |-  ( ( F : A --> B /\ dom F = A ) -> F Fn A )
4 dffn4 
 |-  ( F Fn A <-> F : A -onto-> ran F )
5 3 4 sylib 
 |-  ( ( F : A --> B /\ dom F = A ) -> F : A -onto-> ran F )
6 imaeq2 
 |-  ( A = dom F -> ( F " A ) = ( F " dom F ) )
7 imadmrn 
 |-  ( F " dom F ) = ran F
8 6 7 eqtrdi 
 |-  ( A = dom F -> ( F " A ) = ran F )
9 8 eqcoms 
 |-  ( dom F = A -> ( F " A ) = ran F )
10 9 adantl 
 |-  ( ( F : A --> B /\ dom F = A ) -> ( F " A ) = ran F )
11 foeq3 
 |-  ( ( F " A ) = ran F -> ( F : A -onto-> ( F " A ) <-> F : A -onto-> ran F ) )
12 10 11 syl 
 |-  ( ( F : A --> B /\ dom F = A ) -> ( F : A -onto-> ( F " A ) <-> F : A -onto-> ran F ) )
13 5 12 mpbird 
 |-  ( ( F : A --> B /\ dom F = A ) -> F : A -onto-> ( F " A ) )
14 1 13 mpdan 
 |-  ( F : A --> B -> F : A -onto-> ( F " A ) )