Theorem ofrn

Description: The range of the function operation. (Contributed by Thierry Arnoux, 8-Jan-2017)

	Ref	Expression
Hypotheses	ofrn.1	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	ofrn.2	⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝐵 )
	ofrn.3	⊢ ( 𝜑 → + : ( 𝐵 × 𝐵 ) ⟶ 𝐶 )
	ofrn.4	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
Assertion	ofrn	⊢ ( 𝜑 → ran ( 𝐹 ∘f + 𝐺 ) ⊆ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		ofrn.1	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2		ofrn.2	⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝐵 )
3		ofrn.3	⊢ ( 𝜑 → + : ( 𝐵 × 𝐵 ) ⟶ 𝐶 )
4		ofrn.4	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5	3	fovcdmda	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐶 )
6		inidm	⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
7	5 1 2 4 4 6	off	⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) : 𝐴 ⟶ 𝐶 )
8	7	frnd	⊢ ( 𝜑 → ran ( 𝐹 ∘f + 𝐺 ) ⊆ 𝐶 )