Theorem ofrn2

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

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

Proof

Step	Hyp	Ref	Expression
1		ofrn.1	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2		ofrn.2	⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝐵 )
3		ofrn.3	⊢ ( 𝜑 → + : ( 𝐵 × 𝐵 ) ⟶ 𝐶 )
4		ofrn.4	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5	1	ffnd	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
6		simprl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑧 = ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) ) ) → 𝑎 ∈ 𝐴 )
7		fnfvelrn	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑎 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑎 ) ∈ ran 𝐹 )
8	5 6 7	syl2an2r	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑧 = ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) ) ) → ( 𝐹 ‘ 𝑎 ) ∈ ran 𝐹 )
9	2	ffnd	⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
10		fnfvelrn	⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝑎 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑎 ) ∈ ran 𝐺 )
11	9 6 10	syl2an2r	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑧 = ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) ) ) → ( 𝐺 ‘ 𝑎 ) ∈ ran 𝐺 )
12		simprr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑧 = ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) ) ) → 𝑧 = ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) )
13		rspceov	⊢ ( ( ( 𝐹 ‘ 𝑎 ) ∈ ran 𝐹 ∧ ( 𝐺 ‘ 𝑎 ) ∈ ran 𝐺 ∧ 𝑧 = ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) ) → ∃ 𝑥 ∈ ran 𝐹 ∃ 𝑦 ∈ ran 𝐺 𝑧 = ( 𝑥 + 𝑦 ) )
14	8 11 12 13	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑧 = ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) ) ) → ∃ 𝑥 ∈ ran 𝐹 ∃ 𝑦 ∈ ran 𝐺 𝑧 = ( 𝑥 + 𝑦 ) )
15	14	rexlimdvaa	⊢ ( 𝜑 → ( ∃ 𝑎 ∈ 𝐴 𝑧 = ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) → ∃ 𝑥 ∈ ran 𝐹 ∃ 𝑦 ∈ ran 𝐺 𝑧 = ( 𝑥 + 𝑦 ) ) )
16	15	ss2abdv	⊢ ( 𝜑 → { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) } ⊆ { 𝑧 ∣ ∃ 𝑥 ∈ ran 𝐹 ∃ 𝑦 ∈ ran 𝐺 𝑧 = ( 𝑥 + 𝑦 ) } )
17		inidm	⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
18		eqidd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑎 ) )
19		eqidd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑎 ) = ( 𝐺 ‘ 𝑎 ) )
20	5 9 4 4 17 18 19	offval	⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) = ( 𝑎 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) ) )
21	20	rneqd	⊢ ( 𝜑 → ran ( 𝐹 ∘f + 𝐺 ) = ran ( 𝑎 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) ) )
22		eqid	⊢ ( 𝑎 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) ) = ( 𝑎 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) )
23	22	rnmpt	⊢ ran ( 𝑎 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) ) = { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) }
24	21 23	eqtrdi	⊢ ( 𝜑 → ran ( 𝐹 ∘f + 𝐺 ) = { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) } )
25	3	ffnd	⊢ ( 𝜑 → + Fn ( 𝐵 × 𝐵 ) )
26	1	frnd	⊢ ( 𝜑 → ran 𝐹 ⊆ 𝐵 )
27	2	frnd	⊢ ( 𝜑 → ran 𝐺 ⊆ 𝐵 )
28		xpss12	⊢ ( ( ran 𝐹 ⊆ 𝐵 ∧ ran 𝐺 ⊆ 𝐵 ) → ( ran 𝐹 × ran 𝐺 ) ⊆ ( 𝐵 × 𝐵 ) )
29	26 27 28	syl2anc	⊢ ( 𝜑 → ( ran 𝐹 × ran 𝐺 ) ⊆ ( 𝐵 × 𝐵 ) )
30		ovelimab	⊢ ( ( + Fn ( 𝐵 × 𝐵 ) ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ ( 𝐵 × 𝐵 ) ) → ( 𝑧 ∈ ( + “ ( ran 𝐹 × ran 𝐺 ) ) ↔ ∃ 𝑥 ∈ ran 𝐹 ∃ 𝑦 ∈ ran 𝐺 𝑧 = ( 𝑥 + 𝑦 ) ) )
31	25 29 30	syl2anc	⊢ ( 𝜑 → ( 𝑧 ∈ ( + “ ( ran 𝐹 × ran 𝐺 ) ) ↔ ∃ 𝑥 ∈ ran 𝐹 ∃ 𝑦 ∈ ran 𝐺 𝑧 = ( 𝑥 + 𝑦 ) ) )
32	31	eqabdv	⊢ ( 𝜑 → ( + “ ( ran 𝐹 × ran 𝐺 ) ) = { 𝑧 ∣ ∃ 𝑥 ∈ ran 𝐹 ∃ 𝑦 ∈ ran 𝐺 𝑧 = ( 𝑥 + 𝑦 ) } )
33	16 24 32	3sstr4d	⊢ ( 𝜑 → ran ( 𝐹 ∘f + 𝐺 ) ⊆ ( + “ ( ran 𝐹 × ran 𝐺 ) ) )