Metamath Proof Explorer

Theorem sge0split

Description: Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020)

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

Proof

Step Hyp Ref Expression
1 sge0split.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 sge0split.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3 sge0split.u ⊢ 𝑈 = ( 𝐴 ∪ 𝐵 )
4 sge0split.in0 ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
5 sge0split.f ⊢ ( 𝜑 → 𝐹 : 𝑈 ⟶ ( 0 [,] +∞ ) )
6 1 adantr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → 𝐴 ∈ 𝑉 )
7 2 adantr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → 𝐵 ∈ 𝑊 )
8 4 adantr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → ( 𝐴 ∩ 𝐵 ) = ∅ )
9 5 adantr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → 𝐹 : 𝑈 ⟶ ( 0 [,] +∞ ) )
10 simpr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → ( Σ^ ‘ 𝐹 ) ∈ ℝ )
11 6 7 3 8 9 10 sge0resplit ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → ( Σ^ ‘ 𝐹 ) = ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) + ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) )
12 unexg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∪ 𝐵 ) ∈ V )
13 1 2 12 syl2anc ⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) ∈ V )
14 3 13 eqeltrid ⊢ ( 𝜑 → 𝑈 ∈ V )
15 14 adantr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → 𝑈 ∈ V )
16 15 9 10 sge0ssre ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) ∈ ℝ )
17 15 9 10 sge0ssre ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ∈ ℝ )
18 rexadd ⊢ ( ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) ∈ ℝ ∧ ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ∈ ℝ ) → ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) = ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) + ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) )
19 16 17 18 syl2anc ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) = ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) + ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) )
20 19 eqcomd ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) + ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) = ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) )
21 11 20 eqtrd ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → ( Σ^ ‘ 𝐹 ) = ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) )
22 simpl ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → 𝜑 )
23 simpr ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → ¬ ( Σ^ ‘ 𝐹 ) ∈ ℝ )
24 14 5 sge0repnf ⊢ ( 𝜑 → ( ( Σ^ ‘ 𝐹 ) ∈ ℝ ↔ ¬ ( Σ^ ‘ 𝐹 ) = +∞ ) )
25 24 adantr ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → ( ( Σ^ ‘ 𝐹 ) ∈ ℝ ↔ ¬ ( Σ^ ‘ 𝐹 ) = +∞ ) )
26 23 25 mtbid ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → ¬ ¬ ( Σ^ ‘ 𝐹 ) = +∞ )
27 26 notnotrd ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → ( Σ^ ‘ 𝐹 ) = +∞ )
28 14 5 sge0xrcl ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ∈ ℝ* )
29 28 adantr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) = +∞ ) → ( Σ^ ‘ 𝐹 ) ∈ ℝ* )
30 ssun1 ⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
31 30 3 sseqtrri ⊢ 𝐴 ⊆ 𝑈
32 31 a1i ⊢ ( 𝜑 → 𝐴 ⊆ 𝑈 )
33 5 32 fssresd ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
34 1 33 sge0xrcl ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) ∈ ℝ* )
35 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
36 ssun2 ⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 )
37 36 3 sseqtrri ⊢ 𝐵 ⊆ 𝑈
38 37 a1i ⊢ ( 𝜑 → 𝐵 ⊆ 𝑈 )
39 5 38 fssresd ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ ( 0 [,] +∞ ) )
40 2 39 sge0cl ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ∈ ( 0 [,] +∞ ) )
41 35 40 sselid ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ∈ ℝ* )
42 34 41 xaddcld ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) ∈ ℝ* )
43 42 adantr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) = +∞ ) → ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) ∈ ℝ* )
44 pnfxr ⊢ +∞ ∈ ℝ*
45 eqid ⊢ +∞ = +∞
46 xreqle ⊢ ( ( +∞ ∈ ℝ* ∧ +∞ = +∞ ) → +∞ ≤ +∞ )
47 44 45 46 mp2an ⊢ +∞ ≤ +∞
48 47 a1i ⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → +∞ ≤ +∞ )
49 14 adantr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → 𝑈 ∈ V )
50 5 adantr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → 𝐹 : 𝑈 ⟶ ( 0 [,] +∞ ) )
51 rnresss ⊢ ran ( 𝐹 ↾ 𝐴 ) ⊆ ran 𝐹
52 51 sseli ⊢ ( +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) → +∞ ∈ ran 𝐹 )
53 52 adantl ⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → +∞ ∈ ran 𝐹 )
54 49 50 53 sge0pnfval ⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → ( Σ^ ‘ 𝐹 ) = +∞ )
55 xrge0neqmnf ⊢ ( ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ∈ ( 0 [,] +∞ ) → ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ≠ -∞ )
56 40 55 syl ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ≠ -∞ )
57 xaddpnf2 ⊢ ( ( ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ∈ ℝ* ∧ ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ≠ -∞ ) → ( +∞ +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) = +∞ )
58 41 56 57 syl2anc ⊢ ( 𝜑 → ( +∞ +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) = +∞ )
59 58 eqcomd ⊢ ( 𝜑 → +∞ = ( +∞ +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) )
60 59 adantr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → +∞ = ( +∞ +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) )
61 1 adantr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → 𝐴 ∈ 𝑉 )
62 33 adantr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
63 simpr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) )
64 61 62 63 sge0pnfval ⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) = +∞ )
65 64 oveq1d ⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) = ( +∞ +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) )
66 60 54 65 3eqtr4d ⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → ( Σ^ ‘ 𝐹 ) = ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) )
67 66 54 eqtr3d ⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) = +∞ )
68 54 67 breq12d ⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → ( ( Σ^ ‘ 𝐹 ) ≤ ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) ↔ +∞ ≤ +∞ ) )
69 48 68 mpbird ⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → ( Σ^ ‘ 𝐹 ) ≤ ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) )
70 47 a1i ⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → +∞ ≤ +∞ )
71 14 adantr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → 𝑈 ∈ V )
72 5 adantr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → 𝐹 : 𝑈 ⟶ ( 0 [,] +∞ ) )
73 rnresss ⊢ ran ( 𝐹 ↾ 𝐵 ) ⊆ ran 𝐹
74 73 sseli ⊢ ( +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) → +∞ ∈ ran 𝐹 )
75 74 adantl ⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → +∞ ∈ ran 𝐹 )
76 71 72 75 sge0pnfval ⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( Σ^ ‘ 𝐹 ) = +∞ )
77 2 adantr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → 𝐵 ∈ 𝑊 )
78 39 adantr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ ( 0 [,] +∞ ) )
79 simpr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) )
80 77 78 79 sge0pnfval ⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) = +∞ )
81 80 oveq2d ⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) = ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 +∞ ) )
82 1 33 sge0cl ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) ∈ ( 0 [,] +∞ ) )
83 xrge0neqmnf ⊢ ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) ∈ ( 0 [,] +∞ ) → ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) ≠ -∞ )
84 82 83 syl ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) ≠ -∞ )
85 xaddpnf1 ⊢ ( ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) ∈ ℝ* ∧ ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) ≠ -∞ ) → ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 +∞ ) = +∞ )
86 34 84 85 syl2anc ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 +∞ ) = +∞ )
87 86 adantr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 +∞ ) = +∞ )
88 81 87 eqtrd ⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) = +∞ )
89 76 88 breq12d ⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( ( Σ^ ‘ 𝐹 ) ≤ ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) ↔ +∞ ≤ +∞ ) )
90 70 89 mpbird ⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( Σ^ ‘ 𝐹 ) ≤ ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) )
91 90 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( Σ^ ‘ 𝐹 ) ≤ ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) )
92 simpr ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) → 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
93 vex ⊢ 𝑧 ∈ V
94 eqid ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) = ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
95 94 elrnmpt ⊢ ( 𝑧 ∈ V → ( 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑧 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
96 93 95 ax-mp ⊢ ( 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑧 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
97 92 96 sylib ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) → ∃ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑧 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
98 simp3 ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑧 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → 𝑧 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
99 inss1 ⊢ ( ( 𝑥 ∩ 𝐴 ) ∩ ( 𝑥 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∩ 𝐴 )
100 inss2 ⊢ ( 𝑥 ∩ 𝐴 ) ⊆ 𝐴
101 99 100 sstri ⊢ ( ( 𝑥 ∩ 𝐴 ) ∩ ( 𝑥 ∩ 𝐵 ) ) ⊆ 𝐴
102 inss2 ⊢ ( ( 𝑥 ∩ 𝐴 ) ∩ ( 𝑥 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∩ 𝐵 )
103 inss2 ⊢ ( 𝑥 ∩ 𝐵 ) ⊆ 𝐵
104 102 103 sstri ⊢ ( ( 𝑥 ∩ 𝐴 ) ∩ ( 𝑥 ∩ 𝐵 ) ) ⊆ 𝐵
105 101 104 ssini ⊢ ( ( 𝑥 ∩ 𝐴 ) ∩ ( 𝑥 ∩ 𝐵 ) ) ⊆ ( 𝐴 ∩ 𝐵 )
106 105 a1i ⊢ ( 𝜑 → ( ( 𝑥 ∩ 𝐴 ) ∩ ( 𝑥 ∩ 𝐵 ) ) ⊆ ( 𝐴 ∩ 𝐵 ) )
107 106 4 sseqtrd ⊢ ( 𝜑 → ( ( 𝑥 ∩ 𝐴 ) ∩ ( 𝑥 ∩ 𝐵 ) ) ⊆ ∅ )
108 ss0 ⊢ ( ( ( 𝑥 ∩ 𝐴 ) ∩ ( 𝑥 ∩ 𝐵 ) ) ⊆ ∅ → ( ( 𝑥 ∩ 𝐴 ) ∩ ( 𝑥 ∩ 𝐵 ) ) = ∅ )
109 107 108 syl ⊢ ( 𝜑 → ( ( 𝑥 ∩ 𝐴 ) ∩ ( 𝑥 ∩ 𝐵 ) ) = ∅ )
110 109 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( ( 𝑥 ∩ 𝐴 ) ∩ ( 𝑥 ∩ 𝐵 ) ) = ∅ )
111 indi ⊢ ( 𝑥 ∩ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝑥 ∩ 𝐴 ) ∪ ( 𝑥 ∩ 𝐵 ) )
112 111 eqcomi ⊢ ( ( 𝑥 ∩ 𝐴 ) ∪ ( 𝑥 ∩ 𝐵 ) ) = ( 𝑥 ∩ ( 𝐴 ∪ 𝐵 ) )
113 112 a1i ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → ( ( 𝑥 ∩ 𝐴 ) ∪ ( 𝑥 ∩ 𝐵 ) ) = ( 𝑥 ∩ ( 𝐴 ∪ 𝐵 ) ) )
114 3 eqcomi ⊢ ( 𝐴 ∪ 𝐵 ) = 𝑈
115 114 ineq2i ⊢ ( 𝑥 ∩ ( 𝐴 ∪ 𝐵 ) ) = ( 𝑥 ∩ 𝑈 )
116 115 a1i ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → ( 𝑥 ∩ ( 𝐴 ∪ 𝐵 ) ) = ( 𝑥 ∩ 𝑈 ) )
117 elinel1 ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → 𝑥 ∈ 𝒫 𝑈 )
118 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝑈 → 𝑥 ⊆ 𝑈 )
119 117 118 syl ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → 𝑥 ⊆ 𝑈 )
120 df-ss ⊢ ( 𝑥 ⊆ 𝑈 ↔ ( 𝑥 ∩ 𝑈 ) = 𝑥 )
121 120 biimpi ⊢ ( 𝑥 ⊆ 𝑈 → ( 𝑥 ∩ 𝑈 ) = 𝑥 )
122 119 121 syl ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → ( 𝑥 ∩ 𝑈 ) = 𝑥 )
123 113 116 122 3eqtrrd ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → 𝑥 = ( ( 𝑥 ∩ 𝐴 ) ∪ ( 𝑥 ∩ 𝐵 ) ) )
124 123 adantl ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → 𝑥 = ( ( 𝑥 ∩ 𝐴 ) ∪ ( 𝑥 ∩ 𝐵 ) ) )
125 elinel2 ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → 𝑥 ∈ Fin )
126 125 adantl ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → 𝑥 ∈ Fin )
127 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
128 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → 𝐹 : 𝑈 ⟶ ( 0 [,] +∞ ) )
129 pm4.56 ⊢ ( ( ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ↔ ¬ ( +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ∨ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) )
130 129 biimpi ⊢ ( ( ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ¬ ( +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ∨ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) )
131 elun ⊢ ( +∞ ∈ ( ran ( 𝐹 ↾ 𝐴 ) ∪ ran ( 𝐹 ↾ 𝐵 ) ) ↔ ( +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ∨ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) )
132 130 131 sylnibr ⊢ ( ( ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ¬ +∞ ∈ ( ran ( 𝐹 ↾ 𝐴 ) ∪ ran ( 𝐹 ↾ 𝐵 ) ) )
133 132 adantll ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ¬ +∞ ∈ ( ran ( 𝐹 ↾ 𝐴 ) ∪ ran ( 𝐹 ↾ 𝐵 ) ) )
134 rnresun ⊢ ran ( 𝐹 ↾ ( 𝐴 ∪ 𝐵 ) ) = ( ran ( 𝐹 ↾ 𝐴 ) ∪ ran ( 𝐹 ↾ 𝐵 ) )
135 134 eqcomi ⊢ ( ran ( 𝐹 ↾ 𝐴 ) ∪ ran ( 𝐹 ↾ 𝐵 ) ) = ran ( 𝐹 ↾ ( 𝐴 ∪ 𝐵 ) )
136 135 a1i ⊢ ( 𝜑 → ( ran ( 𝐹 ↾ 𝐴 ) ∪ ran ( 𝐹 ↾ 𝐵 ) ) = ran ( 𝐹 ↾ ( 𝐴 ∪ 𝐵 ) ) )
137 114 reseq2i ⊢ ( 𝐹 ↾ ( 𝐴 ∪ 𝐵 ) ) = ( 𝐹 ↾ 𝑈 )
138 137 rneqi ⊢ ran ( 𝐹 ↾ ( 𝐴 ∪ 𝐵 ) ) = ran ( 𝐹 ↾ 𝑈 )
139 138 a1i ⊢ ( 𝜑 → ran ( 𝐹 ↾ ( 𝐴 ∪ 𝐵 ) ) = ran ( 𝐹 ↾ 𝑈 ) )
140 ffn ⊢ ( 𝐹 : 𝑈 ⟶ ( 0 [,] +∞ ) → 𝐹 Fn 𝑈 )
141 fnresdm ⊢ ( 𝐹 Fn 𝑈 → ( 𝐹 ↾ 𝑈 ) = 𝐹 )
142 5 140 141 3syl ⊢ ( 𝜑 → ( 𝐹 ↾ 𝑈 ) = 𝐹 )
143 142 rneqd ⊢ ( 𝜑 → ran ( 𝐹 ↾ 𝑈 ) = ran 𝐹 )
144 136 139 143 3eqtrd ⊢ ( 𝜑 → ( ran ( 𝐹 ↾ 𝐴 ) ∪ ran ( 𝐹 ↾ 𝐵 ) ) = ran 𝐹 )
145 144 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( ran ( 𝐹 ↾ 𝐴 ) ∪ ran ( 𝐹 ↾ 𝐵 ) ) = ran 𝐹 )
146 133 145 neleqtrd ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ¬ +∞ ∈ ran 𝐹 )
147 128 146 fge0iccico ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → 𝐹 : 𝑈 ⟶ ( 0 [,) +∞ ) )
148 147 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝐹 : 𝑈 ⟶ ( 0 [,) +∞ ) )
149 119 adantr ⊢ ( ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → 𝑥 ⊆ 𝑈 )
150 simpr ⊢ ( ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑥 )
151 149 150 sseldd ⊢ ( ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑈 )
152 151 adantll ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑈 )
153 148 152 ffvelrnd ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,) +∞ ) )
154 127 153 sselid ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
155 154 recnd ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ )
156 110 124 126 155 fsumsplit ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) + Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ) )
157 infi ⊢ ( 𝑥 ∈ Fin → ( 𝑥 ∩ 𝐴 ) ∈ Fin )
158 125 157 syl ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → ( 𝑥 ∩ 𝐴 ) ∈ Fin )
159 158 adantl ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( 𝑥 ∩ 𝐴 ) ∈ Fin )
160 simpl ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ) → ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) )
161 elinel1 ⊢ ( 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) → 𝑦 ∈ 𝑥 )
162 161 adantl ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ) → 𝑦 ∈ 𝑥 )
163 160 162 154 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
164 159 163 fsumrecl ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
165 infi ⊢ ( 𝑥 ∈ Fin → ( 𝑥 ∩ 𝐵 ) ∈ Fin )
166 125 165 syl ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → ( 𝑥 ∩ 𝐵 ) ∈ Fin )
167 166 adantl ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( 𝑥 ∩ 𝐵 ) ∈ Fin )
168 simpl ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ) → ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) )
169 elinel1 ⊢ ( 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) → 𝑦 ∈ 𝑥 )
170 169 adantl ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ) → 𝑦 ∈ 𝑥 )
171 168 170 154 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
172 167 171 fsumrecl ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
173 rexadd ⊢ ( ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ∈ ℝ ∧ Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ∈ ℝ ) → ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) +𝑒 Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ) = ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) + Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ) )
174 164 172 173 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) +𝑒 Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ) = ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) + Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ) )
175 174 eqcomd ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) + Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ) = ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) +𝑒 Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ) )
176 156 175 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) +𝑒 Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ) )
177 ressxr ⊢ ℝ ⊆ ℝ*
178 177 164 sselid ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ∈ ℝ* )
179 177 172 sselid ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ∈ ℝ* )
180 1 adantr ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → 𝐴 ∈ 𝑉 )
181 33 adantr ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
182 simpr ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) )
183 181 182 fge0iccico ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ ( 0 [,) +∞ ) )
184 180 183 sge0reval ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) = sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) )
185 184 eqcomd ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) = ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) )
186 34 adantr ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) ∈ ℝ* )
187 185 186 eqeltrd ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) ∈ ℝ* )
188 187 adantr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) ∈ ℝ* )
189 2 adantr ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → 𝐵 ∈ 𝑊 )
190 39 adantr ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ ( 0 [,] +∞ ) )
191 simpr ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) )
192 190 191 fge0iccico ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ ( 0 [,) +∞ ) )
193 189 192 sge0reval ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) = sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) )
194 193 eqcomd ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) = ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) )
195 41 adantr ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ∈ ℝ* )
196 194 195 eqeltrd ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ∈ ℝ* )
197 196 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ∈ ℝ* )
198 188 197 jca ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) ∈ ℝ* ∧ sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ∈ ℝ* ) )
199 198 adantr ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) ∈ ℝ* ∧ sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ∈ ℝ* ) )
200 178 179 199 jca31 ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ∈ ℝ* ∧ Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ∈ ℝ* ) ∧ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) ∈ ℝ* ∧ sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ∈ ℝ* ) ) )
201 180 adantr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → 𝐴 ∈ 𝑉 )
202 181 adantr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
203 182 adantr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) )
204 202 203 fge0iccico ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ ( 0 [,) +∞ ) )
205 100 a1i ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( 𝑥 ∩ 𝐴 ) ⊆ 𝐴 )
206 158 adantl ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( 𝑥 ∩ 𝐴 ) ∈ Fin )
207 201 204 205 206 fsumlesge0 ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ≤ ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) )
208 100 sseli ⊢ ( 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) → 𝑦 ∈ 𝐴 )
209 fvres ⊢ ( 𝑦 ∈ 𝐴 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
210 208 209 syl ⊢ ( 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
211 210 adantl ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ) → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
212 211 sumeq2dv ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) )
213 184 adantr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) = sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) )
214 212 213 breq12d ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ≤ ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) ↔ Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ≤ sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) ) )
215 207 214 mpbid ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ≤ sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) )
216 215 adantlr ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ≤ sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) )
217 189 adantr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → 𝐵 ∈ 𝑊 )
218 190 adantr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ ( 0 [,] +∞ ) )
219 191 adantr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) )
220 218 219 fge0iccico ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ ( 0 [,) +∞ ) )
221 103 a1i ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( 𝑥 ∩ 𝐵 ) ⊆ 𝐵 )
222 166 adantl ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( 𝑥 ∩ 𝐵 ) ∈ Fin )
223 217 220 221 222 fsumlesge0 ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ≤ ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) )
224 103 sseli ⊢ ( 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) → 𝑦 ∈ 𝐵 )
225 fvres ⊢ ( 𝑦 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
226 224 225 syl ⊢ ( 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
227 226 adantl ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ) → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
228 227 sumeq2dv ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) = Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) )
229 193 adantr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) = sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) )
230 228 229 breq12d ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ≤ ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ↔ Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) )
231 223 230 mpbid ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) )
232 231 adantllr ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) )
233 216 232 jca ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ≤ sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) ∧ Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) )
234 xle2add ⊢ ( ( ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ∈ ℝ* ∧ Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ∈ ℝ* ) ∧ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) ∈ ℝ* ∧ sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ∈ ℝ* ) ) → ( ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ≤ sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) ∧ Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) → ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) +𝑒 Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ) ≤ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) ) )
235 200 233 234 sylc ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) +𝑒 Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ) ≤ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) )
236 176 235 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ≤ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) )
237 236 3adant3 ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑧 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ≤ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) )
238 98 237 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑧 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → 𝑧 ≤ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) )
239 238 3exp ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → ( 𝑧 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) → 𝑧 ≤ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) ) ) )
240 239 rexlimdv ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( ∃ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑧 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) → 𝑧 ≤ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) ) )
241 240 adantr ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) → ( ∃ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑧 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) → 𝑧 ≤ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) ) )
242 97 241 mpd ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) → 𝑧 ≤ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) )
243 242 ralrimiva ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ∀ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) 𝑧 ≤ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) )
244 147 sge0rnre ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ⊆ ℝ )
245 177 a1i ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ℝ ⊆ ℝ* )
246 244 245 sstrd ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ⊆ ℝ* )
247 188 197 xaddcld ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) ∈ ℝ* )
248 supxrleub ⊢ ( ( ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ⊆ ℝ* ∧ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) ∈ ℝ* ) → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) ≤ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) ↔ ∀ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) 𝑧 ≤ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) ) )
249 246 247 248 syl2anc ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) ≤ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) ↔ ∀ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) 𝑧 ≤ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) ) )
250 243 249 mpbird ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) ≤ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) )
251 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → 𝑈 ∈ V )
252 251 147 sge0reval ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( Σ^ ‘ 𝐹 ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) )
253 184 adantr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) = sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) )
254 193 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) = sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) )
255 253 254 oveq12d ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) = ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) )
256 250 252 255 3brtr4d ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( Σ^ ‘ 𝐹 ) ≤ ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) )
257 91 256 pm2.61dan ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → ( Σ^ ‘ 𝐹 ) ≤ ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) )
258 69 257 pm2.61dan ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ≤ ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) )
259 258 adantr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) = +∞ ) → ( Σ^ ‘ 𝐹 ) ≤ ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) )
260 pnfge ⊢ ( ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) ∈ ℝ* → ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) ≤ +∞ )
261 42 260 syl ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) ≤ +∞ )
262 261 adantr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) = +∞ ) → ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) ≤ +∞ )
263 id ⊢ ( ( Σ^ ‘ 𝐹 ) = +∞ → ( Σ^ ‘ 𝐹 ) = +∞ )
264 263 eqcomd ⊢ ( ( Σ^ ‘ 𝐹 ) = +∞ → +∞ = ( Σ^ ‘ 𝐹 ) )
265 264 adantl ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) = +∞ ) → +∞ = ( Σ^ ‘ 𝐹 ) )
266 262 265 breqtrd ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) = +∞ ) → ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) ≤ ( Σ^ ‘ 𝐹 ) )
267 29 43 259 266 xrletrid ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) = +∞ ) → ( Σ^ ‘ 𝐹 ) = ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) )
268 22 27 267 syl2anc ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → ( Σ^ ‘ 𝐹 ) = ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) )
269 21 268 pm2.61dan ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) )