Description: The range of the function operation. (Contributed by Thierry Arnoux, 8-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ofrn.1 | |- ( ph -> F : A --> B ) |
|
ofrn.2 | |- ( ph -> G : A --> B ) |
||
ofrn.3 | |- ( ph -> .+ : ( B X. B ) --> C ) |
||
ofrn.4 | |- ( ph -> A e. V ) |
||
Assertion | ofrn | |- ( ph -> ran ( F oF .+ G ) C_ C ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ofrn.1 | |- ( ph -> F : A --> B ) |
|
2 | ofrn.2 | |- ( ph -> G : A --> B ) |
|
3 | ofrn.3 | |- ( ph -> .+ : ( B X. B ) --> C ) |
|
4 | ofrn.4 | |- ( ph -> A e. V ) |
|
5 | 3 | fovrnda | |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. C ) |
6 | inidm | |- ( A i^i A ) = A |
|
7 | 5 1 2 4 4 6 | off | |- ( ph -> ( F oF .+ G ) : A --> C ) |
8 | 7 | frnd | |- ( ph -> ran ( F oF .+ G ) C_ C ) |