Metamath Proof Explorer

Theorem sge0ltfirp

Description: If the sum of nonnegative extended reals is real, then it can be approximated from below by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0ltfirp.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
sge0ltfirp.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
sge0ltfirp.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ+ )
sge0ltfirp.re ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ∈ ℝ )
Assertion sge0ltfirp ( 𝜑 → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ 𝐹 ) < ( ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) + 𝑌 ) )

Proof

Step Hyp Ref Expression
1 sge0ltfirp.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2 sge0ltfirp.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
3 sge0ltfirp.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ+ )
4 sge0ltfirp.re ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ∈ ℝ )
5 1 2 4 sge0rern ⊢ ( 𝜑 → ¬ +∞ ∈ ran 𝐹 )
6 2 5 fge0iccico ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,) +∞ ) )
7 6 sge0rnre ⊢ ( 𝜑 → ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ⊆ ℝ )
8 sge0rnn0 ⊢ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ≠ ∅
9 8 a1i ⊢ ( 𝜑 → ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ≠ ∅ )
10 1 2 4 sge0rnbnd ⊢ ( 𝜑 → ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) 𝑤 ≤ 𝑧 )
11 7 9 10 3 suprltrp ⊢ ( 𝜑 → ∃ 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < 𝑤 )
12 nfv ⊢ Ⅎ 𝑤 𝜑
13 nfv ⊢ Ⅎ 𝑤 ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ 𝐹 ) < ( ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) + 𝑌 )
14 simp1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ∧ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < 𝑤 ) → 𝜑 )
15 vex ⊢ 𝑤 ∈ V
16 eqid ⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) = ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
17 16 elrnmpt ⊢ ( 𝑤 ∈ V → ( 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
18 15 17 ax-mp ⊢ ( 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
19 18 birani ⊢ ( ( 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ∧ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < 𝑤 ) → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
20 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
21 20 nfrn ⊢ Ⅎ 𝑥 ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
22 nfcv ⊢ Ⅎ 𝑥 ℝ
23 nfcv ⊢ Ⅎ 𝑥 <
24 21 22 23 nfsup ⊢ Ⅎ 𝑥 sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < )
25 nfcv ⊢ Ⅎ 𝑥 −
26 nfcv ⊢ Ⅎ 𝑥 𝑌
27 24 25 26 nfov ⊢ Ⅎ 𝑥 ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 )
28 nfcv ⊢ Ⅎ 𝑥 𝑤
29 27 23 28 nfbr ⊢ Ⅎ 𝑥 ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < 𝑤
30 simpl ⊢ ( ( ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < 𝑤 ∧ 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < 𝑤 )
31 simpr ⊢ ( ( ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < 𝑤 ∧ 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
32 30 31 breqtrd ⊢ ( ( ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < 𝑤 ∧ 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
33 32 ex ⊢ ( ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < 𝑤 → ( 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
34 33 a1d ⊢ ( ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < 𝑤 → ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) → ( 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) )
35 29 34 reximdai ⊢ ( ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < 𝑤 → ( ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
36 35 adantl ⊢ ( ( 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ∧ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < 𝑤 ) → ( ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
37 19 36 mpd ⊢ ( ( 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ∧ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < 𝑤 ) → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
38 37 3adant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ∧ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < 𝑤 ) → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
39 simpl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) )
40 1 2 4 sge0supre ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) )
41 40 oveq1d ⊢ ( 𝜑 → ( ( Σ^ ‘ 𝐹 ) − 𝑌 ) = ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) )
42 41 adantr ⊢ ( ( 𝜑 ∧ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( ( Σ^ ‘ 𝐹 ) − 𝑌 ) = ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) )
43 simpr ⊢ ( ( 𝜑 ∧ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
44 42 43 eqbrtrd ⊢ ( ( 𝜑 ∧ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( ( Σ^ ‘ 𝐹 ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
45 44 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( ( Σ^ ‘ 𝐹 ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
46 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ ( ( Σ^ ‘ 𝐹 ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( ( Σ^ ‘ 𝐹 ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
47 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( Σ^ ‘ 𝐹 ) ∈ ℝ )
48 3 rpred ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
49 48 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑌 ∈ ℝ )
50 elinel2 ⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑥 ∈ Fin )
51 50 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑥 ∈ Fin )
52 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
53 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝐹 : 𝑋 ⟶ ( 0 [,) +∞ ) )
54 53 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝐹 : 𝑋 ⟶ ( 0 [,) +∞ ) )
55 elpwinss ⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑥 ⊆ 𝑋 )
56 55 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑥 ⊆ 𝑋 )
57 56 sselda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑋 )
58 54 57 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,) +∞ ) )
59 52 58 sselid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
60 51 59 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
61 47 49 60 ltsubaddd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( ( ( Σ^ ‘ 𝐹 ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ↔ ( Σ^ ‘ 𝐹 ) < ( Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) + 𝑌 ) ) )
62 61 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ ( ( Σ^ ‘ 𝐹 ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( ( ( Σ^ ‘ 𝐹 ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ↔ ( Σ^ ‘ 𝐹 ) < ( Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) + 𝑌 ) ) )
63 46 62 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ ( ( Σ^ ‘ 𝐹 ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( Σ^ ‘ 𝐹 ) < ( Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) + 𝑌 ) )
64 53 56 fssresd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( 𝐹 ↾ 𝑥 ) : 𝑥 ⟶ ( 0 [,) +∞ ) )
65 51 64 sge0fsum ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) = Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝑥 ) ‘ 𝑦 ) )
66 fvres ⊢ ( 𝑦 ∈ 𝑥 → ( ( 𝐹 ↾ 𝑥 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
67 66 sumeq2i ⊢ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝑥 ) ‘ 𝑦 ) = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 )
68 67 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝑥 ) ‘ 𝑦 ) = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
69 65 68 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) )
70 69 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) + 𝑌 ) = ( ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) + 𝑌 ) )
71 70 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ ( ( Σ^ ‘ 𝐹 ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) + 𝑌 ) = ( ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) + 𝑌 ) )
72 63 71 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ ( ( Σ^ ‘ 𝐹 ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( Σ^ ‘ 𝐹 ) < ( ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) + 𝑌 ) )
73 39 45 72 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( Σ^ ‘ 𝐹 ) < ( ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) + 𝑌 ) )
74 73 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) → ( Σ^ ‘ 𝐹 ) < ( ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) + 𝑌 ) ) )
75 74 reximdva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ 𝐹 ) < ( ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) + 𝑌 ) ) )
76 75 imp ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ 𝐹 ) < ( ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) + 𝑌 ) )
77 14 38 76 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ∧ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < 𝑤 ) → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ 𝐹 ) < ( ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) + 𝑌 ) )
78 77 3exp ⊢ ( 𝜑 → ( 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < 𝑤 → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ 𝐹 ) < ( ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) + 𝑌 ) ) ) )
79 12 13 78 rexlimd ⊢ ( 𝜑 → ( ∃ 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < 𝑤 → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ 𝐹 ) < ( ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) + 𝑌 ) ) )
80 11 79 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ 𝐹 ) < ( ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) + 𝑌 ) )