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