Theorem ofrn2

Description: The range of the function operation. (Contributed by Thierry Arnoux, 21-Mar-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	ofrn2	$$⊢\phi \to \mathrm{ran}\left(F{\underset{\dot{}}{+}}_{f}G\right)\subseteq \underset{\dot{}}{+}\left[\mathrm{ran}F\times \mathrm{ran}G\right]$$

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	1	ffnd	$$⊢\phi \to FFnA$$
6		simprl	$$⊢\left(\phi \wedge \left(a\in A\wedge z=F\left(a\right)\underset{\dot{}}{+}G\left(a\right)\right)\right)\to a\in A$$
7		fnfvelrn	$$⊢\left(FFnA\wedge a\in A\right)\to F\left(a\right)\in \mathrm{ran}F$$
8	5 6 7	syl2an2r	$$⊢\left(\phi \wedge \left(a\in A\wedge z=F\left(a\right)\underset{\dot{}}{+}G\left(a\right)\right)\right)\to F\left(a\right)\in \mathrm{ran}F$$
9	2	ffnd	$$⊢\phi \to GFnA$$
10		fnfvelrn	$$⊢\left(GFnA\wedge a\in A\right)\to G\left(a\right)\in \mathrm{ran}G$$
11	9 6 10	syl2an2r	$$⊢\left(\phi \wedge \left(a\in A\wedge z=F\left(a\right)\underset{\dot{}}{+}G\left(a\right)\right)\right)\to G\left(a\right)\in \mathrm{ran}G$$
12		simprr	$$⊢\left(\phi \wedge \left(a\in A\wedge z=F\left(a\right)\underset{\dot{}}{+}G\left(a\right)\right)\right)\to z=F\left(a\right)\underset{\dot{}}{+}G\left(a\right)$$
13		rspceov	$$⊢\left(F\left(a\right)\in \mathrm{ran}F\wedge G\left(a\right)\in \mathrm{ran}G\wedge z=F\left(a\right)\underset{\dot{}}{+}G\left(a\right)\right)\to \exists x\in \mathrm{ran}F\exists y\in \mathrm{ran}Gz=x\underset{\dot{}}{+}y$$
14	8 11 12 13	syl3anc	$$⊢\left(\phi \wedge \left(a\in A\wedge z=F\left(a\right)\underset{\dot{}}{+}G\left(a\right)\right)\right)\to \exists x\in \mathrm{ran}F\exists y\in \mathrm{ran}Gz=x\underset{\dot{}}{+}y$$
15	14	rexlimdvaa	$$⊢\phi \to \left(\exists a\in Az=F\left(a\right)\underset{\dot{}}{+}G\left(a\right)\to \exists x\in \mathrm{ran}F\exists y\in \mathrm{ran}Gz=x\underset{\dot{}}{+}y\right)$$
16	15	ss2abdv	$$⊢\phi \to \left\{z|\exists a\in Az=F\left(a\right)\underset{\dot{}}{+}G\left(a\right)\right\}\subseteq \left\{z|\exists x\in \mathrm{ran}F\exists y\in \mathrm{ran}Gz=x\underset{\dot{}}{+}y\right\}$$
17		inidm	$$⊢A\cap A=A$$
18		eqidd	$$⊢\left(\phi \wedge a\in A\right)\to F\left(a\right)=F\left(a\right)$$
19		eqidd	$$⊢\left(\phi \wedge a\in A\right)\to G\left(a\right)=G\left(a\right)$$
20	5 9 4 4 17 18 19	offval	$$⊢\phi \to F{\underset{\dot{}}{+}}_{f}G=\left(a\in A⟼F\left(a\right)\underset{\dot{}}{+}G\left(a\right)\right)$$
21	20	rneqd	$$⊢\phi \to \mathrm{ran}\left(F{\underset{\dot{}}{+}}_{f}G\right)=\mathrm{ran}\left(a\in A⟼F\left(a\right)\underset{\dot{}}{+}G\left(a\right)\right)$$
22		eqid	$$⊢\left(a\in A⟼F\left(a\right)\underset{\dot{}}{+}G\left(a\right)\right)=\left(a\in A⟼F\left(a\right)\underset{\dot{}}{+}G\left(a\right)\right)$$
23	22	rnmpt	$$⊢\mathrm{ran}\left(a\in A⟼F\left(a\right)\underset{\dot{}}{+}G\left(a\right)\right)=\left\{z|\exists a\in Az=F\left(a\right)\underset{\dot{}}{+}G\left(a\right)\right\}$$
24	21 23	eqtrdi	$$⊢\phi \to \mathrm{ran}\left(F{\underset{\dot{}}{+}}_{f}G\right)=\left\{z|\exists a\in Az=F\left(a\right)\underset{\dot{}}{+}G\left(a\right)\right\}$$
25	3	ffnd	$$⊢\phi \to \underset{\dot{}}{+}Fn\left(B\times B\right)$$
26	1	frnd	$$⊢\phi \to \mathrm{ran}F\subseteq B$$
27	2	frnd	$$⊢\phi \to \mathrm{ran}G\subseteq B$$
28		xpss12	$$⊢\left(\mathrm{ran}F\subseteq B\wedge \mathrm{ran}G\subseteq B\right)\to \mathrm{ran}F\times \mathrm{ran}G\subseteq B\times B$$
29	26 27 28	syl2anc	$$⊢\phi \to \mathrm{ran}F\times \mathrm{ran}G\subseteq B\times B$$
30		ovelimab	$$⊢\left(\underset{\dot{}}{+}Fn\left(B\times B\right)\wedge \mathrm{ran}F\times \mathrm{ran}G\subseteq B\times B\right)\to \left(z\in \underset{\dot{}}{+}\left[\mathrm{ran}F\times \mathrm{ran}G\right]\leftrightarrow \exists x\in \mathrm{ran}F\exists y\in \mathrm{ran}Gz=x\underset{\dot{}}{+}y\right)$$
31	25 29 30	syl2anc	$$⊢\phi \to \left(z\in \underset{\dot{}}{+}\left[\mathrm{ran}F\times \mathrm{ran}G\right]\leftrightarrow \exists x\in \mathrm{ran}F\exists y\in \mathrm{ran}Gz=x\underset{\dot{}}{+}y\right)$$
32	31	abbi2dv	$$⊢\phi \to \underset{\dot{}}{+}\left[\mathrm{ran}F\times \mathrm{ran}G\right]=\left\{z|\exists x\in \mathrm{ran}F\exists y\in \mathrm{ran}Gz=x\underset{\dot{}}{+}y\right\}$$
33	16 24 32	3sstr4d	$$⊢\phi \to \mathrm{ran}\left(F{\underset{\dot{}}{+}}_{f}G\right)\subseteq \underset{\dot{}}{+}\left[\mathrm{ran}F\times \mathrm{ran}G\right]$$