Theorem ofrn

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

	Ref	Expression
Hypotheses	ofrn.1	$$⊢\phi \to F:A⟶B$$
	ofrn.2	$$⊢\phi \to G:A⟶B$$
	ofrn.3	$$⊢\phi \to \underset{\dot{}}{+}:B\times B⟶C$$
	ofrn.4	$$⊢\phi \to A\in V$$
Assertion	ofrn	$$⊢\phi \to \mathrm{ran}\left(F{\underset{\dot{}}{+}}_{f}G\right)\subseteq C$$

Proof

Step	Hyp	Ref	Expression
1		ofrn.1	$$⊢\phi \to F:A⟶B$$
2		ofrn.2	$$⊢\phi \to G:A⟶B$$
3		ofrn.3	$$⊢\phi \to \underset{\dot{}}{+}:B\times B⟶C$$
4		ofrn.4	$$⊢\phi \to A\in V$$
5	3	fovcdmda	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x\underset{\dot{}}{+}y\in C$$
6		inidm	$$⊢A\cap A=A$$
7	5 1 2 4 4 6	off	$$⊢\phi \to \left(F{\underset{\dot{}}{+}}_{f}G\right):A⟶C$$
8	7	frnd	$$⊢\phi \to \mathrm{ran}\left(F{\underset{\dot{}}{+}}_{f}G\right)\subseteq C$$