Metamath Proof Explorer


Theorem ofrn

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 )

Proof

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 )