Metamath Proof Explorer

Theorem fnrndomg

Description: The range of a function is dominated by its domain. (Contributed by NM, 1-Sep-2004)

Ref Expression
Assertion fnrndomg 
|- ( A e. B -> ( F Fn A -> ran F ~<_ A ) )

Proof

Step Hyp Ref Expression
1 dffn4 
 |-  ( F Fn A <-> F : A -onto-> ran F )
2 fodomg 
 |-  ( A e. B -> ( F : A -onto-> ran F -> ran F ~<_ A ) )
3 1 2 biimtrid 
 |-  ( A e. B -> ( F Fn A -> ran F ~<_ A ) )