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 biimpi ⊢ ( 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
20 19 adantr ⊢ ( ( 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ∧ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < 𝑤 ) → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
21 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
22 21 nfrn ⊢ Ⅎ 𝑥 ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
23 nfcv ⊢ Ⅎ 𝑥 ℝ
24 nfcv ⊢ Ⅎ 𝑥 <
25 22 23 24 nfsup ⊢ Ⅎ 𝑥 sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < )
26 nfcv ⊢ Ⅎ 𝑥 −
27 nfcv ⊢ Ⅎ 𝑥 𝑌
28 25 26 27 nfov ⊢ Ⅎ 𝑥 ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 )
29 nfcv ⊢ Ⅎ 𝑥 𝑤
30 28 24 29 nfbr ⊢ Ⅎ 𝑥 ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < 𝑤
31 simpl ⊢ ( ( ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < 𝑤 ∧ 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < 𝑤 )
32 simpr ⊢ ( ( ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < 𝑤 ∧ 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
33 31 32 breqtrd ⊢ ( ( ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < 𝑤 ∧ 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
34 33 ex ⊢ ( ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < 𝑤 → ( 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
35 34 a1d ⊢ ( ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < 𝑤 → ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) → ( 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) )
36 30 35 reximdai ⊢ ( ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < 𝑤 → ( ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
37 36 adantl ⊢ ( ( 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ∧ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < 𝑤 ) → ( ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑤 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
38 20 37 mpd ⊢ ( ( 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ∧ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < 𝑤 ) → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
39 38 3adant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ∧ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < 𝑤 ) → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
40 simpl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) )
41 1 2 4 sge0supre ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) )
42 41 oveq1d ⊢ ( 𝜑 → ( ( Σ^ ‘ 𝐹 ) − 𝑌 ) = ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) )
43 42 adantr ⊢ ( ( 𝜑 ∧ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( ( Σ^ ‘ 𝐹 ) − 𝑌 ) = ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) )
44 simpr ⊢ ( ( 𝜑 ∧ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
45 43 44 eqbrtrd ⊢ ( ( 𝜑 ∧ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( ( Σ^ ‘ 𝐹 ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
46 45 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( ( Σ^ ‘ 𝐹 ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
47 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ ( ( Σ^ ‘ 𝐹 ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( ( Σ^ ‘ 𝐹 ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
48 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( Σ^ ‘ 𝐹 ) ∈ ℝ )
49 3 rpred ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
50 49 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑌 ∈ ℝ )
51 elinel2 ⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑥 ∈ Fin )
52 51 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑥 ∈ Fin )
53 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
54 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝐹 : 𝑋 ⟶ ( 0 [,) +∞ ) )
55 54 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝐹 : 𝑋 ⟶ ( 0 [,) +∞ ) )
56 elpwinss ⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑥 ⊆ 𝑋 )
57 56 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑥 ⊆ 𝑋 )
58 57 sselda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑋 )
59 55 58 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,) +∞ ) )
60 53 59 sseldi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
61 52 60 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
62 48 50 61 ltsubaddd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( ( ( Σ^ ‘ 𝐹 ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ↔ ( Σ^ ‘ 𝐹 ) < ( Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) + 𝑌 ) ) )
63 62 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ ( ( Σ^ ‘ 𝐹 ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( ( ( Σ^ ‘ 𝐹 ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ↔ ( Σ^ ‘ 𝐹 ) < ( Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) + 𝑌 ) ) )
64 47 63 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ ( ( Σ^ ‘ 𝐹 ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( Σ^ ‘ 𝐹 ) < ( Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) + 𝑌 ) )
65 54 57 fssresd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( 𝐹 ↾ 𝑥 ) : 𝑥 ⟶ ( 0 [,) +∞ ) )
66 52 65 sge0fsum ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) = Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝑥 ) ‘ 𝑦 ) )
67 fvres ⊢ ( 𝑦 ∈ 𝑥 → ( ( 𝐹 ↾ 𝑥 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
68 67 sumeq2i ⊢ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝑥 ) ‘ 𝑦 ) = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 )
69 68 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝑥 ) ‘ 𝑦 ) = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
70 66 69 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) )
71 70 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) + 𝑌 ) = ( ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) + 𝑌 ) )
72 71 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ ( ( Σ^ ‘ 𝐹 ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) + 𝑌 ) = ( ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) + 𝑌 ) )
73 64 72 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ ( ( Σ^ ‘ 𝐹 ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( Σ^ ‘ 𝐹 ) < ( ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) + 𝑌 ) )
74 40 46 73 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( Σ^ ‘ 𝐹 ) < ( ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) + 𝑌 ) )
75 74 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) → ( Σ^ ‘ 𝐹 ) < ( ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) + 𝑌 ) ) )
76 75 reximdva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ 𝐹 ) < ( ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) + 𝑌 ) ) )
77 76 imp ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ 𝐹 ) < ( ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) + 𝑌 ) )
78 14 39 77 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ∧ ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < 𝑤 ) → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ 𝐹 ) < ( ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) + 𝑌 ) )
79 78 3exp ⊢ ( 𝜑 → ( 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < 𝑤 → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ 𝐹 ) < ( ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) + 𝑌 ) ) ) )
80 12 13 79 rexlimd ⊢ ( 𝜑 → ( ∃ 𝑤 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) − 𝑌 ) < 𝑤 → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ 𝐹 ) < ( ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) + 𝑌 ) ) )
81 11 80 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ 𝐹 ) < ( ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) + 𝑌 ) )