Description: The range of a function is dominated by its domain. This theorem requires the axiom of choice ax-ac2 ; see fnrndomnum for a version that does not. (Contributed by NM, 1-Sep-2004) (Proof shortened by Vincent Gonzalez, 17-Aug-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | fnrndomg | |- ( A e. B -> ( F Fn A -> ran F ~<_ A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | numth3 | |- ( A e. B -> A e. dom card ) |
|
| 2 | fnrndomnum | |- ( A e. dom card -> ( F Fn A -> ran F ~<_ A ) ) |
|
| 3 | 1 2 | syl | |- ( A e. B -> ( F Fn A -> ran F ~<_ A ) ) |