Description: The image of the domain of an onto function. (Contributed by NM, 29-Nov-2002)
Ref | Expression | ||
---|---|---|---|
Assertion | foima | |- ( F : A -onto-> B -> ( F " A ) = B ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imadmrn | |- ( F " dom F ) = ran F |
|
2 | fof | |- ( F : A -onto-> B -> F : A --> B ) |
|
3 | 2 | fdmd | |- ( F : A -onto-> B -> dom F = A ) |
4 | 3 | imaeq2d | |- ( F : A -onto-> B -> ( F " dom F ) = ( F " A ) ) |
5 | forn | |- ( F : A -onto-> B -> ran F = B ) |
|
6 | 1 4 5 | 3eqtr3a | |- ( F : A -onto-> B -> ( F " A ) = B ) |