This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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