Metamath Proof Explorer

Theorem sge0resplit

Description: sum^ splits into two parts, when it's a real number. This is a special case of sge0split . (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0resplit.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
sge0resplit.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
sge0resplit.u ⊢ 𝑈 = ( 𝐴 ∪ 𝐵 )
sge0resplit.in0 ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
sge0resplit.f ⊢ ( 𝜑 → 𝐹 : 𝑈 ⟶ ( 0 [,] +∞ ) )
sge0resplit.re ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ∈ ℝ )
Assertion sge0resplit ( 𝜑 → ( Σ^ ‘ 𝐹 ) = ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) + ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 sge0resplit.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 sge0resplit.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3 sge0resplit.u ⊢ 𝑈 = ( 𝐴 ∪ 𝐵 )
4 sge0resplit.in0 ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
5 sge0resplit.f ⊢ ( 𝜑 → 𝐹 : 𝑈 ⟶ ( 0 [,] +∞ ) )
6 sge0resplit.re ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ∈ ℝ )
7 ssun1 ⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
8 3 eqcomi ⊢ ( 𝐴 ∪ 𝐵 ) = 𝑈
9 7 8 sseqtri ⊢ 𝐴 ⊆ 𝑈
10 9 a1i ⊢ ( 𝜑 → 𝐴 ⊆ 𝑈 )
11 5 10 fssresd ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
12 3 a1i ⊢ ( 𝜑 → 𝑈 = ( 𝐴 ∪ 𝐵 ) )
13 unexg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∪ 𝐵 ) ∈ V )
14 1 2 13 syl2anc ⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) ∈ V )
15 12 14 eqeltrd ⊢ ( 𝜑 → 𝑈 ∈ V )
16 15 5 6 sge0ssre ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) ∈ ℝ )
17 1 11 16 sge0supre ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) , ℝ , < ) )
18 17 16 eqeltrrd ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) , ℝ , < ) ∈ ℝ )
19 ssun2 ⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 )
20 19 8 sseqtri ⊢ 𝐵 ⊆ 𝑈
21 20 a1i ⊢ ( 𝜑 → 𝐵 ⊆ 𝑈 )
22 5 21 fssresd ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ ( 0 [,] +∞ ) )
23 15 5 6 sge0ssre ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ∈ ℝ )
24 2 22 23 sge0supre ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) , ℝ , < ) )
25 24 23 eqeltrrd ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) , ℝ , < ) ∈ ℝ )
26 rexadd ⊢ ( ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) , ℝ , < ) ∈ ℝ ∧ sup ( ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) , ℝ , < ) ∈ ℝ ) → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) , ℝ , < ) +𝑒 sup ( ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) , ℝ , < ) ) = ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) , ℝ , < ) + sup ( ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) , ℝ , < ) ) )
27 18 25 26 syl2anc ⊢ ( 𝜑 → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) , ℝ , < ) +𝑒 sup ( ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) , ℝ , < ) ) = ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) , ℝ , < ) + sup ( ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) , ℝ , < ) ) )
28 15 5 6 sge0rern ⊢ ( 𝜑 → ¬ +∞ ∈ ran 𝐹 )
29 nelrnres ⊢ ( ¬ +∞ ∈ ran 𝐹 → ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) )
30 28 29 syl ⊢ ( 𝜑 → ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) )
31 11 30 fge0iccico ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ ( 0 [,) +∞ ) )
32 31 sge0rnre ⊢ ( 𝜑 → ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ⊆ ℝ )
33 sge0rnn0 ⊢ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ≠ ∅
34 33 a1i ⊢ ( 𝜑 → ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ≠ ∅ )
35 1 31 sge0reval ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) , ℝ* , < ) )
36 35 eqcomd ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) , ℝ* , < ) = ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) )
37 36 16 eqeltrd ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) , ℝ* , < ) ∈ ℝ )
38 supxrre3 ⊢ ( ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ⊆ ℝ ∧ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ≠ ∅ ) → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) , ℝ* , < ) ∈ ℝ ↔ ∃ 𝑤 ∈ ℝ ∀ 𝑡 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) 𝑡 ≤ 𝑤 ) )
39 32 34 38 syl2anc ⊢ ( 𝜑 → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) , ℝ* , < ) ∈ ℝ ↔ ∃ 𝑤 ∈ ℝ ∀ 𝑡 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) 𝑡 ≤ 𝑤 ) )
40 37 39 mpbid ⊢ ( 𝜑 → ∃ 𝑤 ∈ ℝ ∀ 𝑡 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) 𝑡 ≤ 𝑤 )
41 nelrnres ⊢ ( ¬ +∞ ∈ ran 𝐹 → ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) )
42 28 41 syl ⊢ ( 𝜑 → ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) )
43 22 42 fge0iccico ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ ( 0 [,) +∞ ) )
44 43 sge0rnre ⊢ ( 𝜑 → ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ⊆ ℝ )
45 sge0rnn0 ⊢ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ≠ ∅
46 45 a1i ⊢ ( 𝜑 → ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ≠ ∅ )
47 2 43 sge0reval ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) , ℝ* , < ) )
48 47 eqcomd ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) , ℝ* , < ) = ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) )
49 48 23 eqeltrd ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) , ℝ* , < ) ∈ ℝ )
50 supxrre3 ⊢ ( ( ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ⊆ ℝ ∧ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ≠ ∅ ) → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) , ℝ* , < ) ∈ ℝ ↔ ∃ 𝑤 ∈ ℝ ∀ 𝑡 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑡 ≤ 𝑤 ) )
51 44 46 50 syl2anc ⊢ ( 𝜑 → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) , ℝ* , < ) ∈ ℝ ↔ ∃ 𝑤 ∈ ℝ ∀ 𝑡 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑡 ≤ 𝑤 ) )
52 49 51 mpbid ⊢ ( 𝜑 → ∃ 𝑤 ∈ ℝ ∀ 𝑡 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑡 ≤ 𝑤 )
53 eqid ⊢ { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) } = { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) }
54 32 34 40 44 46 52 53 supadd ⊢ ( 𝜑 → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) , ℝ , < ) + sup ( ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) , ℝ , < ) ) = sup ( { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) } , ℝ , < ) )
55 simpl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) } ) → 𝜑 )
56 vex ⊢ 𝑟 ∈ V
57 eqeq1 ⊢ ( 𝑧 = 𝑟 → ( 𝑧 = ( 𝑣 + 𝑢 ) ↔ 𝑟 = ( 𝑣 + 𝑢 ) ) )
58 57 rexbidv ⊢ ( 𝑧 = 𝑟 → ( ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) ↔ ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( 𝑣 + 𝑢 ) ) )
59 58 rexbidv ⊢ ( 𝑧 = 𝑟 → ( ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) ↔ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( 𝑣 + 𝑢 ) ) )
60 56 59 elab ⊢ ( 𝑟 ∈ { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) } ↔ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( 𝑣 + 𝑢 ) )
61 60 bilani ⊢ ( ( 𝜑 ∧ 𝑟 ∈ { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) } ) → ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( 𝑣 + 𝑢 ) )
62 simpl ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∧ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) ) → 𝜑 )
63 vex ⊢ 𝑣 ∈ V
64 sumeq1 ⊢ ( 𝑥 = 𝑎 → Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) )
65 64 cbvmptv ⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) = ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) )
66 65 elrnmpt ⊢ ( 𝑣 ∈ V → ( 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ↔ ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) )
67 63 66 ax-mp ⊢ ( 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ↔ ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) )
68 67 birani ⊢ ( ( 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∧ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) → ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) )
69 vex ⊢ 𝑢 ∈ V
70 sumeq1 ⊢ ( 𝑥 = 𝑏 → Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) )
71 70 cbvmptv ⊢ ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) = ( 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) )
72 71 elrnmpt ⊢ ( 𝑢 ∈ V → ( 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ↔ ∃ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) )
73 69 72 ax-mp ⊢ ( 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ↔ ∃ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) )
74 73 bilani ⊢ ( ( 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∧ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) → ∃ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) )
75 68 74 jca ⊢ ( ( 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∧ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) → ( ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ ∃ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) )
76 reeanv ⊢ ( ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∃ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ↔ ( ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ ∃ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) )
77 75 76 sylibr ⊢ ( ( 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∧ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) → ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∃ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) )
78 77 adantl ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∧ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) ) → ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∃ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) )
79 eqid ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) = ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
80 elinel1 ⊢ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑎 ∈ 𝒫 𝐴 )
81 elpwi ⊢ ( 𝑎 ∈ 𝒫 𝐴 → 𝑎 ⊆ 𝐴 )
82 id ⊢ ( 𝑎 ⊆ 𝐴 → 𝑎 ⊆ 𝐴 )
83 82 9 sstrdi ⊢ ( 𝑎 ⊆ 𝐴 → 𝑎 ⊆ 𝑈 )
84 81 83 syl ⊢ ( 𝑎 ∈ 𝒫 𝐴 → 𝑎 ⊆ 𝑈 )
85 80 84 syl ⊢ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑎 ⊆ 𝑈 )
86 85 adantr ⊢ ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → 𝑎 ⊆ 𝑈 )
87 elinel1 ⊢ ( 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) → 𝑏 ∈ 𝒫 𝐵 )
88 elpwi ⊢ ( 𝑏 ∈ 𝒫 𝐵 → 𝑏 ⊆ 𝐵 )
89 id ⊢ ( 𝑏 ⊆ 𝐵 → 𝑏 ⊆ 𝐵 )
90 89 20 sstrdi ⊢ ( 𝑏 ⊆ 𝐵 → 𝑏 ⊆ 𝑈 )
91 88 90 syl ⊢ ( 𝑏 ∈ 𝒫 𝐵 → 𝑏 ⊆ 𝑈 )
92 87 91 syl ⊢ ( 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) → 𝑏 ⊆ 𝑈 )
93 92 adantl ⊢ ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → 𝑏 ⊆ 𝑈 )
94 86 93 unssd ⊢ ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → ( 𝑎 ∪ 𝑏 ) ⊆ 𝑈 )
95 vex ⊢ 𝑎 ∈ V
96 vex ⊢ 𝑏 ∈ V
97 95 96 unex ⊢ ( 𝑎 ∪ 𝑏 ) ∈ V
98 97 elpw ⊢ ( ( 𝑎 ∪ 𝑏 ) ∈ 𝒫 𝑈 ↔ ( 𝑎 ∪ 𝑏 ) ⊆ 𝑈 )
99 94 98 sylibr ⊢ ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → ( 𝑎 ∪ 𝑏 ) ∈ 𝒫 𝑈 )
100 elinel2 ⊢ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑎 ∈ Fin )
101 100 adantr ⊢ ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → 𝑎 ∈ Fin )
102 elinel2 ⊢ ( 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) → 𝑏 ∈ Fin )
103 102 adantl ⊢ ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → 𝑏 ∈ Fin )
104 unfi ⊢ ( ( 𝑎 ∈ Fin ∧ 𝑏 ∈ Fin ) → ( 𝑎 ∪ 𝑏 ) ∈ Fin )
105 101 103 104 syl2anc ⊢ ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → ( 𝑎 ∪ 𝑏 ) ∈ Fin )
106 99 105 elind ⊢ ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → ( 𝑎 ∪ 𝑏 ) ∈ ( 𝒫 𝑈 ∩ Fin ) )
107 106 adantl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) → ( 𝑎 ∪ 𝑏 ) ∈ ( 𝒫 𝑈 ∩ Fin ) )
108 107 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) ∧ ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) ∧ 𝑟 = ( 𝑣 + 𝑢 ) ) → ( 𝑎 ∪ 𝑏 ) ∈ ( 𝒫 𝑈 ∩ Fin ) )
109 simpl ⊢ ( ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) → 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) )
110 simpr ⊢ ( ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) → 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) )
111 109 110 oveq12d ⊢ ( ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) → ( 𝑣 + 𝑢 ) = ( Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) + Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) )
112 111 adantl ⊢ ( ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ∧ ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) → ( 𝑣 + 𝑢 ) = ( Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) + Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) )
113 80 81 syl ⊢ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑎 ⊆ 𝐴 )
114 113 sselda ⊢ ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑦 ∈ 𝑎 ) → 𝑦 ∈ 𝐴 )
115 fvres ⊢ ( 𝑦 ∈ 𝐴 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
116 114 115 syl ⊢ ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑦 ∈ 𝑎 ) → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
117 116 sumeq2dv ⊢ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) → Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = Σ 𝑦 ∈ 𝑎 ( 𝐹 ‘ 𝑦 ) )
118 117 adantr ⊢ ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = Σ 𝑦 ∈ 𝑎 ( 𝐹 ‘ 𝑦 ) )
119 87 88 syl ⊢ ( 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) → 𝑏 ⊆ 𝐵 )
120 119 sselda ⊢ ( ( 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ 𝑦 ∈ 𝑏 ) → 𝑦 ∈ 𝐵 )
121 fvres ⊢ ( 𝑦 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
122 120 121 syl ⊢ ( ( 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ 𝑦 ∈ 𝑏 ) → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
123 122 sumeq2dv ⊢ ( 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) → Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) = Σ 𝑦 ∈ 𝑏 ( 𝐹 ‘ 𝑦 ) )
124 123 adantl ⊢ ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) = Σ 𝑦 ∈ 𝑏 ( 𝐹 ‘ 𝑦 ) )
125 118 124 oveq12d ⊢ ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → ( Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) + Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) = ( Σ 𝑦 ∈ 𝑎 ( 𝐹 ‘ 𝑦 ) + Σ 𝑦 ∈ 𝑏 ( 𝐹 ‘ 𝑦 ) ) )
126 125 adantr ⊢ ( ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ∧ ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) → ( Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) + Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) = ( Σ 𝑦 ∈ 𝑎 ( 𝐹 ‘ 𝑦 ) + Σ 𝑦 ∈ 𝑏 ( 𝐹 ‘ 𝑦 ) ) )
127 112 126 eqtrd ⊢ ( ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ∧ ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) → ( 𝑣 + 𝑢 ) = ( Σ 𝑦 ∈ 𝑎 ( 𝐹 ‘ 𝑦 ) + Σ 𝑦 ∈ 𝑏 ( 𝐹 ‘ 𝑦 ) ) )
128 127 ad4ant23 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) ∧ ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) ∧ 𝑟 = ( 𝑣 + 𝑢 ) ) → ( 𝑣 + 𝑢 ) = ( Σ 𝑦 ∈ 𝑎 ( 𝐹 ‘ 𝑦 ) + Σ 𝑦 ∈ 𝑏 ( 𝐹 ‘ 𝑦 ) ) )
129 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) ∧ ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) ∧ 𝑟 = ( 𝑣 + 𝑢 ) ) → 𝑟 = ( 𝑣 + 𝑢 ) )
130 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) → ( 𝐴 ∩ 𝐵 ) = ∅ )
131 113 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) → 𝑎 ⊆ 𝐴 )
132 119 adantl ⊢ ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → 𝑏 ⊆ 𝐵 )
133 132 adantl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) → 𝑏 ⊆ 𝐵 )
134 ssin0 ⊢ ( ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝑎 ⊆ 𝐴 ∧ 𝑏 ⊆ 𝐵 ) → ( 𝑎 ∩ 𝑏 ) = ∅ )
135 130 131 133 134 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) → ( 𝑎 ∩ 𝑏 ) = ∅ )
136 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) → ( 𝑎 ∪ 𝑏 ) = ( 𝑎 ∪ 𝑏 ) )
137 105 adantl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) → ( 𝑎 ∪ 𝑏 ) ∈ Fin )
138 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
139 ax-resscn ⊢ ℝ ⊆ ℂ
140 138 139 sstri ⊢ ( 0 [,) +∞ ) ⊆ ℂ
141 5 28 fge0iccico ⊢ ( 𝜑 → 𝐹 : 𝑈 ⟶ ( 0 [,) +∞ ) )
142 141 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) ∧ 𝑦 ∈ ( 𝑎 ∪ 𝑏 ) ) → 𝐹 : 𝑈 ⟶ ( 0 [,) +∞ ) )
143 94 sselda ⊢ ( ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ∧ 𝑦 ∈ ( 𝑎 ∪ 𝑏 ) ) → 𝑦 ∈ 𝑈 )
144 143 adantll ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) ∧ 𝑦 ∈ ( 𝑎 ∪ 𝑏 ) ) → 𝑦 ∈ 𝑈 )
145 142 144 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) ∧ 𝑦 ∈ ( 𝑎 ∪ 𝑏 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,) +∞ ) )
146 140 145 sselid ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) ∧ 𝑦 ∈ ( 𝑎 ∪ 𝑏 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ )
147 135 136 137 146 fsumsplit ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) → Σ 𝑦 ∈ ( 𝑎 ∪ 𝑏 ) ( 𝐹 ‘ 𝑦 ) = ( Σ 𝑦 ∈ 𝑎 ( 𝐹 ‘ 𝑦 ) + Σ 𝑦 ∈ 𝑏 ( 𝐹 ‘ 𝑦 ) ) )
148 147 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) ∧ ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) ∧ 𝑟 = ( 𝑣 + 𝑢 ) ) → Σ 𝑦 ∈ ( 𝑎 ∪ 𝑏 ) ( 𝐹 ‘ 𝑦 ) = ( Σ 𝑦 ∈ 𝑎 ( 𝐹 ‘ 𝑦 ) + Σ 𝑦 ∈ 𝑏 ( 𝐹 ‘ 𝑦 ) ) )
149 128 129 148 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) ∧ ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) ∧ 𝑟 = ( 𝑣 + 𝑢 ) ) → 𝑟 = Σ 𝑦 ∈ ( 𝑎 ∪ 𝑏 ) ( 𝐹 ‘ 𝑦 ) )
150 sumeq1 ⊢ ( 𝑥 = ( 𝑎 ∪ 𝑏 ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = Σ 𝑦 ∈ ( 𝑎 ∪ 𝑏 ) ( 𝐹 ‘ 𝑦 ) )
151 150 rspceeqv ⊢ ( ( ( 𝑎 ∪ 𝑏 ) ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑟 = Σ 𝑦 ∈ ( 𝑎 ∪ 𝑏 ) ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
152 108 149 151 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) ∧ ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) ∧ 𝑟 = ( 𝑣 + 𝑢 ) ) → ∃ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
153 56 a1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) ∧ ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) ∧ 𝑟 = ( 𝑣 + 𝑢 ) ) → 𝑟 ∈ V )
154 79 152 153 elrnmptd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) ∧ ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) ∧ 𝑟 = ( 𝑣 + 𝑢 ) ) → 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
155 154 ex ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) ∧ ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) → ( 𝑟 = ( 𝑣 + 𝑢 ) → 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) )
156 155 ex ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) → ( ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) → ( 𝑟 = ( 𝑣 + 𝑢 ) → 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) ) )
157 156 ex ⊢ ( 𝜑 → ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → ( ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) → ( 𝑟 = ( 𝑣 + 𝑢 ) → 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) ) ) )
158 157 rexlimdvv ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∃ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) → ( 𝑟 = ( 𝑣 + 𝑢 ) → 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) ) )
159 158 imp ⊢ ( ( 𝜑 ∧ ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∃ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) → ( 𝑟 = ( 𝑣 + 𝑢 ) → 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) )
160 62 78 159 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∧ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) ) → ( 𝑟 = ( 𝑣 + 𝑢 ) → 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) )
161 160 ex ⊢ ( 𝜑 → ( ( 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∧ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) → ( 𝑟 = ( 𝑣 + 𝑢 ) → 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) ) )
162 161 rexlimdvv ⊢ ( 𝜑 → ( ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( 𝑣 + 𝑢 ) → 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) )
163 162 imp ⊢ ( ( 𝜑 ∧ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( 𝑣 + 𝑢 ) ) → 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
164 55 61 163 syl2anc ⊢ ( ( 𝜑 ∧ 𝑟 ∈ { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) } ) → 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
165 164 ex ⊢ ( 𝜑 → ( 𝑟 ∈ { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) } → 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) )
166 79 elrnmpt ⊢ ( 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
167 166 ibi ⊢ ( 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
168 167 adantl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) → ∃ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
169 nfv ⊢ Ⅎ 𝑥 𝜑
170 nfcv ⊢ Ⅎ 𝑥 𝑟
171 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
172 171 nfrn ⊢ Ⅎ 𝑥 ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
173 170 172 nfel ⊢ Ⅎ 𝑥 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
174 169 173 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
175 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) )
176 175 nfrn ⊢ Ⅎ 𝑥 ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) )
177 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) )
178 177 nfrn ⊢ Ⅎ 𝑥 ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) )
179 nfv ⊢ Ⅎ 𝑥 𝑟 = ( 𝑣 + 𝑢 )
180 178 179 nfrexw ⊢ Ⅎ 𝑥 ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( 𝑣 + 𝑢 )
181 176 180 nfrexw ⊢ Ⅎ 𝑥 ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( 𝑣 + 𝑢 )
182 inss2 ⊢ ( 𝑥 ∩ 𝐴 ) ⊆ 𝐴
183 182 sseli ⊢ ( 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) → 𝑦 ∈ 𝐴 )
184 183 adantl ⊢ ( ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ) → 𝑦 ∈ 𝐴 )
185 115 eqcomd ⊢ ( 𝑦 ∈ 𝐴 → ( 𝐹 ‘ 𝑦 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) )
186 184 185 syl ⊢ ( ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ) → ( 𝐹 ‘ 𝑦 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) )
187 186 sumeq2dv ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) = Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) )
188 sumeq1 ⊢ ( 𝑥 = 𝑧 → Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = Σ 𝑦 ∈ 𝑧 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) )
189 188 cbvmptv ⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) = ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑧 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) )
190 vex ⊢ 𝑥 ∈ V
191 190 inex1 ⊢ ( 𝑥 ∩ 𝐴 ) ∈ V
192 191 elpw ⊢ ( ( 𝑥 ∩ 𝐴 ) ∈ 𝒫 𝐴 ↔ ( 𝑥 ∩ 𝐴 ) ⊆ 𝐴 )
193 182 192 mpbir ⊢ ( 𝑥 ∩ 𝐴 ) ∈ 𝒫 𝐴
194 193 a1i ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → ( 𝑥 ∩ 𝐴 ) ∈ 𝒫 𝐴 )
195 elinel2 ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → 𝑥 ∈ Fin )
196 inss1 ⊢ ( 𝑥 ∩ 𝐴 ) ⊆ 𝑥
197 196 a1i ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → ( 𝑥 ∩ 𝐴 ) ⊆ 𝑥 )
198 ssfi ⊢ ( ( 𝑥 ∈ Fin ∧ ( 𝑥 ∩ 𝐴 ) ⊆ 𝑥 ) → ( 𝑥 ∩ 𝐴 ) ∈ Fin )
199 195 197 198 syl2anc ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → ( 𝑥 ∩ 𝐴 ) ∈ Fin )
200 194 199 elind ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → ( 𝑥 ∩ 𝐴 ) ∈ ( 𝒫 𝐴 ∩ Fin ) )
201 eqidd ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) )
202 sumeq1 ⊢ ( 𝑧 = ( 𝑥 ∩ 𝐴 ) → Σ 𝑦 ∈ 𝑧 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) )
203 202 rspceeqv ⊢ ( ( ( 𝑥 ∩ 𝐴 ) ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) → ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = Σ 𝑦 ∈ 𝑧 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) )
204 200 201 203 syl2anc ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = Σ 𝑦 ∈ 𝑧 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) )
205 sumex ⊢ Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∈ V
206 205 a1i ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∈ V )
207 189 204 206 elrnmptd ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) )
208 187 207 eqeltrd ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) )
209 208 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) )
210 sumeq1 ⊢ ( 𝑥 = 𝑧 → Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) = Σ 𝑦 ∈ 𝑧 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) )
211 210 cbvmptv ⊢ ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) = ( 𝑧 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑧 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) )
212 inss2 ⊢ ( 𝑥 ∩ 𝐵 ) ⊆ 𝐵
213 190 inex1 ⊢ ( 𝑥 ∩ 𝐵 ) ∈ V
214 213 elpw ⊢ ( ( 𝑥 ∩ 𝐵 ) ∈ 𝒫 𝐵 ↔ ( 𝑥 ∩ 𝐵 ) ⊆ 𝐵 )
215 212 214 mpbir ⊢ ( 𝑥 ∩ 𝐵 ) ∈ 𝒫 𝐵
216 215 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑥 ∩ 𝐵 ) ∈ 𝒫 𝐵 )
217 inss1 ⊢ ( 𝑥 ∩ 𝐵 ) ⊆ 𝑥
218 217 a1i ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → ( 𝑥 ∩ 𝐵 ) ⊆ 𝑥 )
219 ssfi ⊢ ( ( 𝑥 ∈ Fin ∧ ( 𝑥 ∩ 𝐵 ) ⊆ 𝑥 ) → ( 𝑥 ∩ 𝐵 ) ∈ Fin )
220 195 218 219 syl2anc ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → ( 𝑥 ∩ 𝐵 ) ∈ Fin )
221 220 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑥 ∩ 𝐵 ) ∈ Fin )
222 216 221 elind ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑥 ∩ 𝐵 ) ∈ ( 𝒫 𝐵 ∩ Fin ) )
223 212 sseli ⊢ ( 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) → 𝑦 ∈ 𝐵 )
224 121 eqcomd ⊢ ( 𝑦 ∈ 𝐵 → ( 𝐹 ‘ 𝑦 ) = ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) )
225 223 224 syl ⊢ ( 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) → ( 𝐹 ‘ 𝑦 ) = ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) )
226 225 sumeq2i ⊢ Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) = Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 )
227 226 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) = Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) )
228 227 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) = Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) )
229 sumeq1 ⊢ ( 𝑧 = ( 𝑥 ∩ 𝐵 ) → Σ 𝑦 ∈ 𝑧 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) = Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) )
230 229 rspceeqv ⊢ ( ( ( 𝑥 ∩ 𝐵 ) ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) = Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) → ∃ 𝑧 ∈ ( 𝒫 𝐵 ∩ Fin ) Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) = Σ 𝑦 ∈ 𝑧 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) )
231 222 228 230 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑧 ∈ ( 𝒫 𝐵 ∩ Fin ) Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) = Σ 𝑦 ∈ 𝑧 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) )
232 sumex ⊢ Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ∈ V
233 232 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ∈ V )
234 211 231 233 elrnmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) )
235 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
236 182 a1i ⊢ ( 𝜑 → ( 𝑥 ∩ 𝐴 ) ⊆ 𝐴 )
237 212 a1i ⊢ ( 𝜑 → ( 𝑥 ∩ 𝐵 ) ⊆ 𝐵 )
238 ssin0 ⊢ ( ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ ( 𝑥 ∩ 𝐴 ) ⊆ 𝐴 ∧ ( 𝑥 ∩ 𝐵 ) ⊆ 𝐵 ) → ( ( 𝑥 ∩ 𝐴 ) ∩ ( 𝑥 ∩ 𝐵 ) ) = ∅ )
239 4 236 237 238 syl3anc ⊢ ( 𝜑 → ( ( 𝑥 ∩ 𝐴 ) ∩ ( 𝑥 ∩ 𝐵 ) ) = ∅ )
240 239 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( ( 𝑥 ∩ 𝐴 ) ∩ ( 𝑥 ∩ 𝐵 ) ) = ∅ )
241 elinel1 ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → 𝑥 ∈ 𝒫 𝑈 )
242 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝑈 → 𝑥 ⊆ 𝑈 )
243 241 242 syl ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → 𝑥 ⊆ 𝑈 )
244 3 ineq2i ⊢ ( 𝑥 ∩ 𝑈 ) = ( 𝑥 ∩ ( 𝐴 ∪ 𝐵 ) )
245 244 a1i ⊢ ( 𝑥 ⊆ 𝑈 → ( 𝑥 ∩ 𝑈 ) = ( 𝑥 ∩ ( 𝐴 ∪ 𝐵 ) ) )
246 dfss ⊢ ( 𝑥 ⊆ 𝑈 ↔ 𝑥 = ( 𝑥 ∩ 𝑈 ) )
247 246 biimpi ⊢ ( 𝑥 ⊆ 𝑈 → 𝑥 = ( 𝑥 ∩ 𝑈 ) )
248 indi ⊢ ( 𝑥 ∩ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝑥 ∩ 𝐴 ) ∪ ( 𝑥 ∩ 𝐵 ) )
249 248 eqcomi ⊢ ( ( 𝑥 ∩ 𝐴 ) ∪ ( 𝑥 ∩ 𝐵 ) ) = ( 𝑥 ∩ ( 𝐴 ∪ 𝐵 ) )
250 249 a1i ⊢ ( 𝑥 ⊆ 𝑈 → ( ( 𝑥 ∩ 𝐴 ) ∪ ( 𝑥 ∩ 𝐵 ) ) = ( 𝑥 ∩ ( 𝐴 ∪ 𝐵 ) ) )
251 245 247 250 3eqtr4d ⊢ ( 𝑥 ⊆ 𝑈 → 𝑥 = ( ( 𝑥 ∩ 𝐴 ) ∪ ( 𝑥 ∩ 𝐵 ) ) )
252 243 251 syl ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → 𝑥 = ( ( 𝑥 ∩ 𝐴 ) ∪ ( 𝑥 ∩ 𝐵 ) ) )
253 252 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → 𝑥 = ( ( 𝑥 ∩ 𝐴 ) ∪ ( 𝑥 ∩ 𝐵 ) ) )
254 195 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → 𝑥 ∈ Fin )
255 141 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝐹 : 𝑈 ⟶ ( 0 [,) +∞ ) )
256 243 sselda ⊢ ( ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑈 )
257 256 adantll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑈 )
258 255 257 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,) +∞ ) )
259 140 258 sselid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ )
260 240 253 254 259 fsumsplit ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) + Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ) )
261 260 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) + Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ) )
262 235 261 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → 𝑟 = ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) + Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ) )
263 oveq2 ⊢ ( 𝑢 = Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) → ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) + 𝑢 ) = ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) + Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ) )
264 263 rspceeqv ⊢ ( ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ∧ 𝑟 = ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) + Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ) ) → ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) + 𝑢 ) )
265 234 262 264 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) + 𝑢 ) )
266 oveq1 ⊢ ( 𝑣 = Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) → ( 𝑣 + 𝑢 ) = ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) + 𝑢 ) )
267 266 eqeq2d ⊢ ( 𝑣 = Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) → ( 𝑟 = ( 𝑣 + 𝑢 ) ↔ 𝑟 = ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) + 𝑢 ) ) )
268 267 rexbidv ⊢ ( 𝑣 = Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) → ( ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( 𝑣 + 𝑢 ) ↔ ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) + 𝑢 ) ) )
269 268 rspcev ⊢ ( ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∧ ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) + 𝑢 ) ) → ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( 𝑣 + 𝑢 ) )
270 209 265 269 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( 𝑣 + 𝑢 ) )
271 270 3exp ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → ( 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) → ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( 𝑣 + 𝑢 ) ) ) )
272 271 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → ( 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) → ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( 𝑣 + 𝑢 ) ) ) )
273 174 181 272 rexlimd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) → ( ∃ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) → ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( 𝑣 + 𝑢 ) ) )
274 168 273 mpd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) → ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( 𝑣 + 𝑢 ) )
275 274 60 sylibr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) → 𝑟 ∈ { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) } )
276 275 ex ⊢ ( 𝜑 → ( 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → 𝑟 ∈ { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) } ) )
277 165 276 impbid ⊢ ( 𝜑 → ( 𝑟 ∈ { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) } ↔ 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) )
278 277 alrimiv ⊢ ( 𝜑 → ∀ 𝑟 ( 𝑟 ∈ { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) } ↔ 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) )
279 dfcleq ⊢ ( { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) } = ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑟 ( 𝑟 ∈ { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) } ↔ 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) )
280 278 279 sylibr ⊢ ( 𝜑 → { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) } = ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
281 280 supeq1d ⊢ ( 𝜑 → sup ( { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) } , ℝ , < ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) )
282 27 54 281 3eqtrrd ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) = ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) , ℝ , < ) +𝑒 sup ( ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) , ℝ , < ) ) )
283 15 5 6 sge0supre ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) )
284 17 24 oveq12d ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) = ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) , ℝ , < ) +𝑒 sup ( ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) , ℝ , < ) ) )
285 282 283 284 3eqtr4d ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) )
286 rexadd ⊢ ( ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) ∈ ℝ ∧ ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ∈ ℝ ) → ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) = ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) + ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) )
287 16 23 286 syl2anc ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) = ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) + ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) )
288 285 287 eqtrd ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) + ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) )