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