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 syl5bi
 |-  ( A e. B -> ( F Fn A -> ran F ~<_ A ) )