Metamath Proof Explorer


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 abbi2dv ( 𝜑 → ( + “ ( ran 𝐹 × ran 𝐺 ) ) = { 𝑧 ∣ ∃ 𝑥 ∈ ran 𝐹𝑦 ∈ ran 𝐺 𝑧 = ( 𝑥 + 𝑦 ) } )
33 16 24 32 3sstr4d ( 𝜑 → ran ( 𝐹f + 𝐺 ) ⊆ ( + “ ( ran 𝐹 × ran 𝐺 ) ) )