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 )