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 vex ⊢ 𝑧 ∈ V
93 eqid ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) = ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
94 93 elrnmpt ⊢ ( 𝑧 ∈ V → ( 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑧 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
95 92 94 ax-mp ⊢ ( 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑧 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
96 95 bilani ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) → ∃ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑧 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
97 simp3 ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑧 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → 𝑧 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
98 inss1 ⊢ ( ( 𝑥 ∩ 𝐴 ) ∩ ( 𝑥 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∩ 𝐴 )
99 inss2 ⊢ ( 𝑥 ∩ 𝐴 ) ⊆ 𝐴
100 98 99 sstri ⊢ ( ( 𝑥 ∩ 𝐴 ) ∩ ( 𝑥 ∩ 𝐵 ) ) ⊆ 𝐴
101 inss2 ⊢ ( ( 𝑥 ∩ 𝐴 ) ∩ ( 𝑥 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∩ 𝐵 )
102 inss2 ⊢ ( 𝑥 ∩ 𝐵 ) ⊆ 𝐵
103 101 102 sstri ⊢ ( ( 𝑥 ∩ 𝐴 ) ∩ ( 𝑥 ∩ 𝐵 ) ) ⊆ 𝐵
104 100 103 ssini ⊢ ( ( 𝑥 ∩ 𝐴 ) ∩ ( 𝑥 ∩ 𝐵 ) ) ⊆ ( 𝐴 ∩ 𝐵 )
105 104 a1i ⊢ ( 𝜑 → ( ( 𝑥 ∩ 𝐴 ) ∩ ( 𝑥 ∩ 𝐵 ) ) ⊆ ( 𝐴 ∩ 𝐵 ) )
106 105 4 sseqtrd ⊢ ( 𝜑 → ( ( 𝑥 ∩ 𝐴 ) ∩ ( 𝑥 ∩ 𝐵 ) ) ⊆ ∅ )
107 ss0 ⊢ ( ( ( 𝑥 ∩ 𝐴 ) ∩ ( 𝑥 ∩ 𝐵 ) ) ⊆ ∅ → ( ( 𝑥 ∩ 𝐴 ) ∩ ( 𝑥 ∩ 𝐵 ) ) = ∅ )
108 106 107 syl ⊢ ( 𝜑 → ( ( 𝑥 ∩ 𝐴 ) ∩ ( 𝑥 ∩ 𝐵 ) ) = ∅ )
109 108 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( ( 𝑥 ∩ 𝐴 ) ∩ ( 𝑥 ∩ 𝐵 ) ) = ∅ )
110 indi ⊢ ( 𝑥 ∩ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝑥 ∩ 𝐴 ) ∪ ( 𝑥 ∩ 𝐵 ) )
111 110 eqcomi ⊢ ( ( 𝑥 ∩ 𝐴 ) ∪ ( 𝑥 ∩ 𝐵 ) ) = ( 𝑥 ∩ ( 𝐴 ∪ 𝐵 ) )
112 111 a1i ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → ( ( 𝑥 ∩ 𝐴 ) ∪ ( 𝑥 ∩ 𝐵 ) ) = ( 𝑥 ∩ ( 𝐴 ∪ 𝐵 ) ) )
113 3 eqcomi ⊢ ( 𝐴 ∪ 𝐵 ) = 𝑈
114 113 ineq2i ⊢ ( 𝑥 ∩ ( 𝐴 ∪ 𝐵 ) ) = ( 𝑥 ∩ 𝑈 )
115 114 a1i ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → ( 𝑥 ∩ ( 𝐴 ∪ 𝐵 ) ) = ( 𝑥 ∩ 𝑈 ) )
116 elinel1 ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → 𝑥 ∈ 𝒫 𝑈 )
117 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝑈 → 𝑥 ⊆ 𝑈 )
118 116 117 syl ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → 𝑥 ⊆ 𝑈 )
119 dfss2 ⊢ ( 𝑥 ⊆ 𝑈 ↔ ( 𝑥 ∩ 𝑈 ) = 𝑥 )
120 119 biimpi ⊢ ( 𝑥 ⊆ 𝑈 → ( 𝑥 ∩ 𝑈 ) = 𝑥 )
121 118 120 syl ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → ( 𝑥 ∩ 𝑈 ) = 𝑥 )
122 112 115 121 3eqtrrd ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → 𝑥 = ( ( 𝑥 ∩ 𝐴 ) ∪ ( 𝑥 ∩ 𝐵 ) ) )
123 122 adantl ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → 𝑥 = ( ( 𝑥 ∩ 𝐴 ) ∪ ( 𝑥 ∩ 𝐵 ) ) )
124 elinel2 ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → 𝑥 ∈ Fin )
125 124 adantl ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → 𝑥 ∈ Fin )
126 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
127 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → 𝐹 : 𝑈 ⟶ ( 0 [,] +∞ ) )
128 pm4.56 ⊢ ( ( ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ↔ ¬ ( +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ∨ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) )
129 128 biimpi ⊢ ( ( ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ¬ ( +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ∨ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) )
130 elun ⊢ ( +∞ ∈ ( ran ( 𝐹 ↾ 𝐴 ) ∪ ran ( 𝐹 ↾ 𝐵 ) ) ↔ ( +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ∨ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) )
131 129 130 sylnibr ⊢ ( ( ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ¬ +∞ ∈ ( ran ( 𝐹 ↾ 𝐴 ) ∪ ran ( 𝐹 ↾ 𝐵 ) ) )
132 131 adantll ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ¬ +∞ ∈ ( ran ( 𝐹 ↾ 𝐴 ) ∪ ran ( 𝐹 ↾ 𝐵 ) ) )
133 rnresun ⊢ ran ( 𝐹 ↾ ( 𝐴 ∪ 𝐵 ) ) = ( ran ( 𝐹 ↾ 𝐴 ) ∪ ran ( 𝐹 ↾ 𝐵 ) )
134 133 eqcomi ⊢ ( ran ( 𝐹 ↾ 𝐴 ) ∪ ran ( 𝐹 ↾ 𝐵 ) ) = ran ( 𝐹 ↾ ( 𝐴 ∪ 𝐵 ) )
135 134 a1i ⊢ ( 𝜑 → ( ran ( 𝐹 ↾ 𝐴 ) ∪ ran ( 𝐹 ↾ 𝐵 ) ) = ran ( 𝐹 ↾ ( 𝐴 ∪ 𝐵 ) ) )
136 113 reseq2i ⊢ ( 𝐹 ↾ ( 𝐴 ∪ 𝐵 ) ) = ( 𝐹 ↾ 𝑈 )
137 136 rneqi ⊢ ran ( 𝐹 ↾ ( 𝐴 ∪ 𝐵 ) ) = ran ( 𝐹 ↾ 𝑈 )
138 137 a1i ⊢ ( 𝜑 → ran ( 𝐹 ↾ ( 𝐴 ∪ 𝐵 ) ) = ran ( 𝐹 ↾ 𝑈 ) )
139 ffn ⊢ ( 𝐹 : 𝑈 ⟶ ( 0 [,] +∞ ) → 𝐹 Fn 𝑈 )
140 fnresdm ⊢ ( 𝐹 Fn 𝑈 → ( 𝐹 ↾ 𝑈 ) = 𝐹 )
141 5 139 140 3syl ⊢ ( 𝜑 → ( 𝐹 ↾ 𝑈 ) = 𝐹 )
142 141 rneqd ⊢ ( 𝜑 → ran ( 𝐹 ↾ 𝑈 ) = ran 𝐹 )
143 135 138 142 3eqtrd ⊢ ( 𝜑 → ( ran ( 𝐹 ↾ 𝐴 ) ∪ ran ( 𝐹 ↾ 𝐵 ) ) = ran 𝐹 )
144 143 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( ran ( 𝐹 ↾ 𝐴 ) ∪ ran ( 𝐹 ↾ 𝐵 ) ) = ran 𝐹 )
145 132 144 neleqtrd ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ¬ +∞ ∈ ran 𝐹 )
146 127 145 fge0iccico ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → 𝐹 : 𝑈 ⟶ ( 0 [,) +∞ ) )
147 146 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝐹 : 𝑈 ⟶ ( 0 [,) +∞ ) )
148 118 adantr ⊢ ( ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → 𝑥 ⊆ 𝑈 )
149 simpr ⊢ ( ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑥 )
150 148 149 sseldd ⊢ ( ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑈 )
151 150 adantll ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑈 )
152 147 151 ffvelcdmd ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,) +∞ ) )
153 126 152 sselid ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
154 153 recnd ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ )
155 109 123 125 154 fsumsplit ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) + Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ) )
156 infi ⊢ ( 𝑥 ∈ Fin → ( 𝑥 ∩ 𝐴 ) ∈ Fin )
157 124 156 syl ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → ( 𝑥 ∩ 𝐴 ) ∈ Fin )
158 157 adantl ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( 𝑥 ∩ 𝐴 ) ∈ Fin )
159 simpl ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ) → ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) )
160 elinel1 ⊢ ( 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) → 𝑦 ∈ 𝑥 )
161 160 adantl ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ) → 𝑦 ∈ 𝑥 )
162 159 161 153 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
163 158 162 fsumrecl ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
164 infi ⊢ ( 𝑥 ∈ Fin → ( 𝑥 ∩ 𝐵 ) ∈ Fin )
165 124 164 syl ⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → ( 𝑥 ∩ 𝐵 ) ∈ Fin )
166 165 adantl ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( 𝑥 ∩ 𝐵 ) ∈ Fin )
167 simpl ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ) → ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) )
168 elinel1 ⊢ ( 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) → 𝑦 ∈ 𝑥 )
169 168 adantl ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ) → 𝑦 ∈ 𝑥 )
170 167 169 153 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
171 166 170 fsumrecl ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
172 rexadd ⊢ ( ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ∈ ℝ ∧ Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ∈ ℝ ) → ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) +𝑒 Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ) = ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) + Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ) )
173 163 171 172 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) +𝑒 Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ) = ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) + Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ) )
174 173 eqcomd ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) + Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ) = ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) +𝑒 Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ) )
175 155 174 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) +𝑒 Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ) )
176 ressxr ⊢ ℝ ⊆ ℝ*
177 176 163 sselid ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ∈ ℝ* )
178 176 171 sselid ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ∈ ℝ* )
179 1 adantr ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → 𝐴 ∈ 𝑉 )
180 33 adantr ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
181 simpr ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) )
182 180 181 fge0iccico ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ ( 0 [,) +∞ ) )
183 179 182 sge0reval ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) = sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) )
184 183 eqcomd ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) = ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) )
185 34 adantr ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) ∈ ℝ* )
186 184 185 eqeltrd ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) ∈ ℝ* )
187 186 adantr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) ∈ ℝ* )
188 2 adantr ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → 𝐵 ∈ 𝑊 )
189 39 adantr ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ ( 0 [,] +∞ ) )
190 simpr ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) )
191 189 190 fge0iccico ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ ( 0 [,) +∞ ) )
192 188 191 sge0reval ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) = sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) )
193 192 eqcomd ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) = ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) )
194 41 adantr ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ∈ ℝ* )
195 193 194 eqeltrd ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ∈ ℝ* )
196 195 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ∈ ℝ* )
197 187 196 jca ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) ∈ ℝ* ∧ sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ∈ ℝ* ) )
198 197 adantr ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) ∈ ℝ* ∧ sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ∈ ℝ* ) )
199 177 178 198 jca31 ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ∈ ℝ* ∧ Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ∈ ℝ* ) ∧ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) ∈ ℝ* ∧ sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ∈ ℝ* ) ) )
200 179 adantr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → 𝐴 ∈ 𝑉 )
201 180 adantr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
202 181 adantr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) )
203 201 202 fge0iccico ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ ( 0 [,) +∞ ) )
204 99 a1i ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( 𝑥 ∩ 𝐴 ) ⊆ 𝐴 )
205 157 adantl ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( 𝑥 ∩ 𝐴 ) ∈ Fin )
206 200 203 204 205 fsumlesge0 ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ≤ ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) )
207 99 sseli ⊢ ( 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) → 𝑦 ∈ 𝐴 )
208 fvres ⊢ ( 𝑦 ∈ 𝐴 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
209 207 208 syl ⊢ ( 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
210 209 adantl ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ) → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
211 210 sumeq2dv ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) )
212 183 adantr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) = sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) )
213 211 212 breq12d ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ≤ ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) ↔ Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ≤ sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) ) )
214 206 213 mpbid ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ≤ sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) )
215 214 adantlr ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ≤ sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) )
216 188 adantr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → 𝐵 ∈ 𝑊 )
217 189 adantr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ ( 0 [,] +∞ ) )
218 190 adantr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) )
219 217 218 fge0iccico ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ ( 0 [,) +∞ ) )
220 102 a1i ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( 𝑥 ∩ 𝐵 ) ⊆ 𝐵 )
221 165 adantl ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( 𝑥 ∩ 𝐵 ) ∈ Fin )
222 216 219 220 221 fsumlesge0 ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ≤ ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) )
223 102 sseli ⊢ ( 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) → 𝑦 ∈ 𝐵 )
224 fvres ⊢ ( 𝑦 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
225 223 224 syl ⊢ ( 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
226 225 adantl ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ) → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
227 226 sumeq2dv ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) = Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) )
228 192 adantr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) = sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) )
229 227 228 breq12d ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ≤ ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ↔ Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) )
230 222 229 mpbid ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) )
231 230 adantllr ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) )
232 215 231 jca ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ≤ sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) ∧ Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) )
233 xle2add ⊢ ( ( ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ∈ ℝ* ∧ Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ∈ ℝ* ) ∧ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) ∈ ℝ* ∧ sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ∈ ℝ* ) ) → ( ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ≤ sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) ∧ Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) → ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) +𝑒 Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ) ≤ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) ) )
234 199 232 233 sylc ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) +𝑒 Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ) ≤ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) )
235 175 234 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ≤ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) )
236 235 3adant3 ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑧 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ≤ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) )
237 97 236 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑧 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → 𝑧 ≤ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) )
238 237 3exp ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → ( 𝑧 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) → 𝑧 ≤ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) ) ) )
239 238 rexlimdv ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( ∃ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑧 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) → 𝑧 ≤ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) ) )
240 239 adantr ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) → ( ∃ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑧 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) → 𝑧 ≤ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) ) )
241 96 240 mpd ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) ∧ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) → 𝑧 ≤ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) )
242 241 ralrimiva ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ∀ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) 𝑧 ≤ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) )
243 146 sge0rnre ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ⊆ ℝ )
244 176 a1i ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ℝ ⊆ ℝ* )
245 243 244 sstrd ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ⊆ ℝ* )
246 187 196 xaddcld ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) ∈ ℝ* )
247 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 ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) ) )
248 245 246 247 syl2anc ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) ≤ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) ↔ ∀ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) 𝑧 ≤ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) ) )
249 242 248 mpbird ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) ≤ ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) )
250 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → 𝑈 ∈ V )
251 250 146 sge0reval ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( Σ^ ‘ 𝐹 ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) )
252 183 adantr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) = sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) )
253 192 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) = sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) )
254 252 253 oveq12d ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) = ( sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑏 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ) , ℝ* , < ) +𝑒 sup ( ran ( 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑑 ∈ 𝑐 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑑 ) ) , ℝ* , < ) ) )
255 249 251 254 3brtr4d ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) → ( Σ^ ‘ 𝐹 ) ≤ ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) )
256 91 255 pm2.61dan ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) → ( Σ^ ‘ 𝐹 ) ≤ ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) )
257 69 256 pm2.61dan ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ≤ ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) )
258 257 adantr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) = +∞ ) → ( Σ^ ‘ 𝐹 ) ≤ ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) )
259 pnfge ⊢ ( ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) ∈ ℝ* → ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) ≤ +∞ )
260 42 259 syl ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) ≤ +∞ )
261 260 adantr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) = +∞ ) → ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) ≤ +∞ )
262 id ⊢ ( ( Σ^ ‘ 𝐹 ) = +∞ → ( Σ^ ‘ 𝐹 ) = +∞ )
263 262 eqcomd ⊢ ( ( Σ^ ‘ 𝐹 ) = +∞ → +∞ = ( Σ^ ‘ 𝐹 ) )
264 263 adantl ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) = +∞ ) → +∞ = ( Σ^ ‘ 𝐹 ) )
265 261 264 breqtrd ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) = +∞ ) → ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) ≤ ( Σ^ ‘ 𝐹 ) )
266 29 43 258 265 xrletrid ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) = +∞ ) → ( Σ^ ‘ 𝐹 ) = ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) )
267 22 27 266 syl2anc ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → ( Σ^ ‘ 𝐹 ) = ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) )
268 21 267 pm2.61dan ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) )