Metamath Proof Explorer


Theorem i1faddlem

Description: Decompose the preimage of a sum. (Contributed by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses i1fadd.1 ( 𝜑𝐹 ∈ dom ∫1 )
i1fadd.2 ( 𝜑𝐺 ∈ dom ∫1 )
Assertion i1faddlem ( ( 𝜑𝐴 ∈ ℂ ) → ( ( 𝐹f + 𝐺 ) “ { 𝐴 } ) = 𝑦 ∈ ran 𝐺 ( ( 𝐹 “ { ( 𝐴𝑦 ) } ) ∩ ( 𝐺 “ { 𝑦 } ) ) )

Proof

Step Hyp Ref Expression
1 i1fadd.1 ( 𝜑𝐹 ∈ dom ∫1 )
2 i1fadd.2 ( 𝜑𝐺 ∈ dom ∫1 )
3 i1ff ( 𝐹 ∈ dom ∫1𝐹 : ℝ ⟶ ℝ )
4 1 3 syl ( 𝜑𝐹 : ℝ ⟶ ℝ )
5 4 ffnd ( 𝜑𝐹 Fn ℝ )
6 i1ff ( 𝐺 ∈ dom ∫1𝐺 : ℝ ⟶ ℝ )
7 2 6 syl ( 𝜑𝐺 : ℝ ⟶ ℝ )
8 7 ffnd ( 𝜑𝐺 Fn ℝ )
9 reex ℝ ∈ V
10 9 a1i ( 𝜑 → ℝ ∈ V )
11 inidm ( ℝ ∩ ℝ ) = ℝ
12 5 8 10 10 11 offn ( 𝜑 → ( 𝐹f + 𝐺 ) Fn ℝ )
13 12 adantr ( ( 𝜑𝐴 ∈ ℂ ) → ( 𝐹f + 𝐺 ) Fn ℝ )
14 fniniseg ( ( 𝐹f + 𝐺 ) Fn ℝ → ( 𝑧 ∈ ( ( 𝐹f + 𝐺 ) “ { 𝐴 } ) ↔ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) )
15 13 14 syl ( ( 𝜑𝐴 ∈ ℂ ) → ( 𝑧 ∈ ( ( 𝐹f + 𝐺 ) “ { 𝐴 } ) ↔ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) )
16 8 ad2antrr ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → 𝐺 Fn ℝ )
17 simprl ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → 𝑧 ∈ ℝ )
18 fnfvelrn ( ( 𝐺 Fn ℝ ∧ 𝑧 ∈ ℝ ) → ( 𝐺𝑧 ) ∈ ran 𝐺 )
19 16 17 18 syl2anc ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → ( 𝐺𝑧 ) ∈ ran 𝐺 )
20 simprr ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 )
21 eqidd ( ( 𝜑𝑧 ∈ ℝ ) → ( 𝐹𝑧 ) = ( 𝐹𝑧 ) )
22 eqidd ( ( 𝜑𝑧 ∈ ℝ ) → ( 𝐺𝑧 ) = ( 𝐺𝑧 ) )
23 5 8 10 10 11 21 22 ofval ( ( 𝜑𝑧 ∈ ℝ ) → ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = ( ( 𝐹𝑧 ) + ( 𝐺𝑧 ) ) )
24 23 ad2ant2r ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = ( ( 𝐹𝑧 ) + ( 𝐺𝑧 ) ) )
25 20 24 eqtr3d ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → 𝐴 = ( ( 𝐹𝑧 ) + ( 𝐺𝑧 ) ) )
26 25 oveq1d ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → ( 𝐴 − ( 𝐺𝑧 ) ) = ( ( ( 𝐹𝑧 ) + ( 𝐺𝑧 ) ) − ( 𝐺𝑧 ) ) )
27 ax-resscn ℝ ⊆ ℂ
28 fss ( ( 𝐹 : ℝ ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐹 : ℝ ⟶ ℂ )
29 4 27 28 sylancl ( 𝜑𝐹 : ℝ ⟶ ℂ )
30 29 ad2antrr ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → 𝐹 : ℝ ⟶ ℂ )
31 30 17 ffvelrnd ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → ( 𝐹𝑧 ) ∈ ℂ )
32 fss ( ( 𝐺 : ℝ ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐺 : ℝ ⟶ ℂ )
33 7 27 32 sylancl ( 𝜑𝐺 : ℝ ⟶ ℂ )
34 33 ad2antrr ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → 𝐺 : ℝ ⟶ ℂ )
35 34 17 ffvelrnd ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → ( 𝐺𝑧 ) ∈ ℂ )
36 31 35 pncand ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → ( ( ( 𝐹𝑧 ) + ( 𝐺𝑧 ) ) − ( 𝐺𝑧 ) ) = ( 𝐹𝑧 ) )
37 26 36 eqtr2d ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → ( 𝐹𝑧 ) = ( 𝐴 − ( 𝐺𝑧 ) ) )
38 5 ad2antrr ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → 𝐹 Fn ℝ )
39 fniniseg ( 𝐹 Fn ℝ → ( 𝑧 ∈ ( 𝐹 “ { ( 𝐴 − ( 𝐺𝑧 ) ) } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐹𝑧 ) = ( 𝐴 − ( 𝐺𝑧 ) ) ) ) )
40 38 39 syl ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → ( 𝑧 ∈ ( 𝐹 “ { ( 𝐴 − ( 𝐺𝑧 ) ) } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐹𝑧 ) = ( 𝐴 − ( 𝐺𝑧 ) ) ) ) )
41 17 37 40 mpbir2and ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → 𝑧 ∈ ( 𝐹 “ { ( 𝐴 − ( 𝐺𝑧 ) ) } ) )
42 eqidd ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → ( 𝐺𝑧 ) = ( 𝐺𝑧 ) )
43 fniniseg ( 𝐺 Fn ℝ → ( 𝑧 ∈ ( 𝐺 “ { ( 𝐺𝑧 ) } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐺𝑧 ) = ( 𝐺𝑧 ) ) ) )
44 16 43 syl ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → ( 𝑧 ∈ ( 𝐺 “ { ( 𝐺𝑧 ) } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐺𝑧 ) = ( 𝐺𝑧 ) ) ) )
45 17 42 44 mpbir2and ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → 𝑧 ∈ ( 𝐺 “ { ( 𝐺𝑧 ) } ) )
46 41 45 elind ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → 𝑧 ∈ ( ( 𝐹 “ { ( 𝐴 − ( 𝐺𝑧 ) ) } ) ∩ ( 𝐺 “ { ( 𝐺𝑧 ) } ) ) )
47 oveq2 ( 𝑦 = ( 𝐺𝑧 ) → ( 𝐴𝑦 ) = ( 𝐴 − ( 𝐺𝑧 ) ) )
48 47 sneqd ( 𝑦 = ( 𝐺𝑧 ) → { ( 𝐴𝑦 ) } = { ( 𝐴 − ( 𝐺𝑧 ) ) } )
49 48 imaeq2d ( 𝑦 = ( 𝐺𝑧 ) → ( 𝐹 “ { ( 𝐴𝑦 ) } ) = ( 𝐹 “ { ( 𝐴 − ( 𝐺𝑧 ) ) } ) )
50 sneq ( 𝑦 = ( 𝐺𝑧 ) → { 𝑦 } = { ( 𝐺𝑧 ) } )
51 50 imaeq2d ( 𝑦 = ( 𝐺𝑧 ) → ( 𝐺 “ { 𝑦 } ) = ( 𝐺 “ { ( 𝐺𝑧 ) } ) )
52 49 51 ineq12d ( 𝑦 = ( 𝐺𝑧 ) → ( ( 𝐹 “ { ( 𝐴𝑦 ) } ) ∩ ( 𝐺 “ { 𝑦 } ) ) = ( ( 𝐹 “ { ( 𝐴 − ( 𝐺𝑧 ) ) } ) ∩ ( 𝐺 “ { ( 𝐺𝑧 ) } ) ) )
53 52 eleq2d ( 𝑦 = ( 𝐺𝑧 ) → ( 𝑧 ∈ ( ( 𝐹 “ { ( 𝐴𝑦 ) } ) ∩ ( 𝐺 “ { 𝑦 } ) ) ↔ 𝑧 ∈ ( ( 𝐹 “ { ( 𝐴 − ( 𝐺𝑧 ) ) } ) ∩ ( 𝐺 “ { ( 𝐺𝑧 ) } ) ) ) )
54 53 rspcev ( ( ( 𝐺𝑧 ) ∈ ran 𝐺𝑧 ∈ ( ( 𝐹 “ { ( 𝐴 − ( 𝐺𝑧 ) ) } ) ∩ ( 𝐺 “ { ( 𝐺𝑧 ) } ) ) ) → ∃ 𝑦 ∈ ran 𝐺 𝑧 ∈ ( ( 𝐹 “ { ( 𝐴𝑦 ) } ) ∩ ( 𝐺 “ { 𝑦 } ) ) )
55 19 46 54 syl2anc ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → ∃ 𝑦 ∈ ran 𝐺 𝑧 ∈ ( ( 𝐹 “ { ( 𝐴𝑦 ) } ) ∩ ( 𝐺 “ { 𝑦 } ) ) )
56 55 ex ( ( 𝜑𝐴 ∈ ℂ ) → ( ( 𝑧 ∈ ℝ ∧ ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) → ∃ 𝑦 ∈ ran 𝐺 𝑧 ∈ ( ( 𝐹 “ { ( 𝐴𝑦 ) } ) ∩ ( 𝐺 “ { 𝑦 } ) ) ) )
57 elin ( 𝑧 ∈ ( ( 𝐹 “ { ( 𝐴𝑦 ) } ) ∩ ( 𝐺 “ { 𝑦 } ) ) ↔ ( 𝑧 ∈ ( 𝐹 “ { ( 𝐴𝑦 ) } ) ∧ 𝑧 ∈ ( 𝐺 “ { 𝑦 } ) ) )
58 5 adantr ( ( 𝜑𝐴 ∈ ℂ ) → 𝐹 Fn ℝ )
59 fniniseg ( 𝐹 Fn ℝ → ( 𝑧 ∈ ( 𝐹 “ { ( 𝐴𝑦 ) } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐹𝑧 ) = ( 𝐴𝑦 ) ) ) )
60 58 59 syl ( ( 𝜑𝐴 ∈ ℂ ) → ( 𝑧 ∈ ( 𝐹 “ { ( 𝐴𝑦 ) } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐹𝑧 ) = ( 𝐴𝑦 ) ) ) )
61 8 adantr ( ( 𝜑𝐴 ∈ ℂ ) → 𝐺 Fn ℝ )
62 fniniseg ( 𝐺 Fn ℝ → ( 𝑧 ∈ ( 𝐺 “ { 𝑦 } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐺𝑧 ) = 𝑦 ) ) )
63 61 62 syl ( ( 𝜑𝐴 ∈ ℂ ) → ( 𝑧 ∈ ( 𝐺 “ { 𝑦 } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐺𝑧 ) = 𝑦 ) ) )
64 60 63 anbi12d ( ( 𝜑𝐴 ∈ ℂ ) → ( ( 𝑧 ∈ ( 𝐹 “ { ( 𝐴𝑦 ) } ) ∧ 𝑧 ∈ ( 𝐺 “ { 𝑦 } ) ) ↔ ( ( 𝑧 ∈ ℝ ∧ ( 𝐹𝑧 ) = ( 𝐴𝑦 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝐺𝑧 ) = 𝑦 ) ) ) )
65 anandi ( ( 𝑧 ∈ ℝ ∧ ( ( 𝐹𝑧 ) = ( 𝐴𝑦 ) ∧ ( 𝐺𝑧 ) = 𝑦 ) ) ↔ ( ( 𝑧 ∈ ℝ ∧ ( 𝐹𝑧 ) = ( 𝐴𝑦 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝐺𝑧 ) = 𝑦 ) ) )
66 simprl ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹𝑧 ) = ( 𝐴𝑦 ) ∧ ( 𝐺𝑧 ) = 𝑦 ) ) ) → 𝑧 ∈ ℝ )
67 23 ad2ant2r ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹𝑧 ) = ( 𝐴𝑦 ) ∧ ( 𝐺𝑧 ) = 𝑦 ) ) ) → ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = ( ( 𝐹𝑧 ) + ( 𝐺𝑧 ) ) )
68 simprrl ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹𝑧 ) = ( 𝐴𝑦 ) ∧ ( 𝐺𝑧 ) = 𝑦 ) ) ) → ( 𝐹𝑧 ) = ( 𝐴𝑦 ) )
69 simprrr ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹𝑧 ) = ( 𝐴𝑦 ) ∧ ( 𝐺𝑧 ) = 𝑦 ) ) ) → ( 𝐺𝑧 ) = 𝑦 )
70 68 69 oveq12d ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹𝑧 ) = ( 𝐴𝑦 ) ∧ ( 𝐺𝑧 ) = 𝑦 ) ) ) → ( ( 𝐹𝑧 ) + ( 𝐺𝑧 ) ) = ( ( 𝐴𝑦 ) + 𝑦 ) )
71 simplr ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹𝑧 ) = ( 𝐴𝑦 ) ∧ ( 𝐺𝑧 ) = 𝑦 ) ) ) → 𝐴 ∈ ℂ )
72 33 ad2antrr ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹𝑧 ) = ( 𝐴𝑦 ) ∧ ( 𝐺𝑧 ) = 𝑦 ) ) ) → 𝐺 : ℝ ⟶ ℂ )
73 72 66 ffvelrnd ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹𝑧 ) = ( 𝐴𝑦 ) ∧ ( 𝐺𝑧 ) = 𝑦 ) ) ) → ( 𝐺𝑧 ) ∈ ℂ )
74 69 73 eqeltrrd ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹𝑧 ) = ( 𝐴𝑦 ) ∧ ( 𝐺𝑧 ) = 𝑦 ) ) ) → 𝑦 ∈ ℂ )
75 71 74 npcand ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹𝑧 ) = ( 𝐴𝑦 ) ∧ ( 𝐺𝑧 ) = 𝑦 ) ) ) → ( ( 𝐴𝑦 ) + 𝑦 ) = 𝐴 )
76 67 70 75 3eqtrd ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹𝑧 ) = ( 𝐴𝑦 ) ∧ ( 𝐺𝑧 ) = 𝑦 ) ) ) → ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 )
77 66 76 jca ( ( ( 𝜑𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹𝑧 ) = ( 𝐴𝑦 ) ∧ ( 𝐺𝑧 ) = 𝑦 ) ) ) → ( 𝑧 ∈ ℝ ∧ ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) )
78 77 ex ( ( 𝜑𝐴 ∈ ℂ ) → ( ( 𝑧 ∈ ℝ ∧ ( ( 𝐹𝑧 ) = ( 𝐴𝑦 ) ∧ ( 𝐺𝑧 ) = 𝑦 ) ) → ( 𝑧 ∈ ℝ ∧ ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) )
79 65 78 syl5bir ( ( 𝜑𝐴 ∈ ℂ ) → ( ( ( 𝑧 ∈ ℝ ∧ ( 𝐹𝑧 ) = ( 𝐴𝑦 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝐺𝑧 ) = 𝑦 ) ) → ( 𝑧 ∈ ℝ ∧ ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) )
80 64 79 sylbid ( ( 𝜑𝐴 ∈ ℂ ) → ( ( 𝑧 ∈ ( 𝐹 “ { ( 𝐴𝑦 ) } ) ∧ 𝑧 ∈ ( 𝐺 “ { 𝑦 } ) ) → ( 𝑧 ∈ ℝ ∧ ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) )
81 57 80 syl5bi ( ( 𝜑𝐴 ∈ ℂ ) → ( 𝑧 ∈ ( ( 𝐹 “ { ( 𝐴𝑦 ) } ) ∩ ( 𝐺 “ { 𝑦 } ) ) → ( 𝑧 ∈ ℝ ∧ ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) )
82 81 rexlimdvw ( ( 𝜑𝐴 ∈ ℂ ) → ( ∃ 𝑦 ∈ ran 𝐺 𝑧 ∈ ( ( 𝐹 “ { ( 𝐴𝑦 ) } ) ∩ ( 𝐺 “ { 𝑦 } ) ) → ( 𝑧 ∈ ℝ ∧ ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) )
83 56 82 impbid ( ( 𝜑𝐴 ∈ ℂ ) → ( ( 𝑧 ∈ ℝ ∧ ( ( 𝐹f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ↔ ∃ 𝑦 ∈ ran 𝐺 𝑧 ∈ ( ( 𝐹 “ { ( 𝐴𝑦 ) } ) ∩ ( 𝐺 “ { 𝑦 } ) ) ) )
84 15 83 bitrd ( ( 𝜑𝐴 ∈ ℂ ) → ( 𝑧 ∈ ( ( 𝐹f + 𝐺 ) “ { 𝐴 } ) ↔ ∃ 𝑦 ∈ ran 𝐺 𝑧 ∈ ( ( 𝐹 “ { ( 𝐴𝑦 ) } ) ∩ ( 𝐺 “ { 𝑦 } ) ) ) )
85 eliun ( 𝑧 𝑦 ∈ ran 𝐺 ( ( 𝐹 “ { ( 𝐴𝑦 ) } ) ∩ ( 𝐺 “ { 𝑦 } ) ) ↔ ∃ 𝑦 ∈ ran 𝐺 𝑧 ∈ ( ( 𝐹 “ { ( 𝐴𝑦 ) } ) ∩ ( 𝐺 “ { 𝑦 } ) ) )
86 84 85 bitr4di ( ( 𝜑𝐴 ∈ ℂ ) → ( 𝑧 ∈ ( ( 𝐹f + 𝐺 ) “ { 𝐴 } ) ↔ 𝑧 𝑦 ∈ ran 𝐺 ( ( 𝐹 “ { ( 𝐴𝑦 ) } ) ∩ ( 𝐺 “ { 𝑦 } ) ) ) )
87 86 eqrdv ( ( 𝜑𝐴 ∈ ℂ ) → ( ( 𝐹f + 𝐺 ) “ { 𝐴 } ) = 𝑦 ∈ ran 𝐺 ( ( 𝐹 “ { ( 𝐴𝑦 ) } ) ∩ ( 𝐺 “ { 𝑦 } ) ) )