Metamath Proof Explorer

Theorem sge0le

Description: If all of the terms of sums compare, so do the sums. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0le.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
sge0le.F ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
sge0le.g ⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ( 0 [,] +∞ ) )
sge0le.le ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) )
Assertion sge0le ( 𝜑 → ( Σ^ ‘ 𝐹 ) ≤ ( Σ^ ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 sge0le.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2 sge0le.F ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
3 sge0le.g ⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ( 0 [,] +∞ ) )
4 sge0le.le ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) )
5 1 2 sge0xrcl ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ∈ ℝ* )
6 pnfge ⊢ ( ( Σ^ ‘ 𝐹 ) ∈ ℝ* → ( Σ^ ‘ 𝐹 ) ≤ +∞ )
7 5 6 syl ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ≤ +∞ )
8 7 adantr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐺 ) = +∞ ) → ( Σ^ ‘ 𝐹 ) ≤ +∞ )
9 id ⊢ ( ( Σ^ ‘ 𝐺 ) = +∞ → ( Σ^ ‘ 𝐺 ) = +∞ )
10 9 eqcomd ⊢ ( ( Σ^ ‘ 𝐺 ) = +∞ → +∞ = ( Σ^ ‘ 𝐺 ) )
11 10 adantl ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐺 ) = +∞ ) → +∞ = ( Σ^ ‘ 𝐺 ) )
12 8 11 breqtrd ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐺 ) = +∞ ) → ( Σ^ ‘ 𝐹 ) ≤ ( Σ^ ‘ 𝐺 ) )
13 elinel2 ⊢ ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑦 ∈ Fin )
14 13 adantl ⊢ ( ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) ∧ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑦 ∈ Fin )
15 2 adantr ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
16 1 adantr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → 𝑋 ∈ 𝑉 )
17 3 adantr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → 𝐺 : 𝑋 ⟶ ( 0 [,] +∞ ) )
18 simpr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → +∞ ∈ ran 𝐹 )
19 2 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝑋 )
20 fvelrnb ⊢ ( 𝐹 Fn 𝑋 → ( +∞ ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) = +∞ ) )
21 19 20 syl ⊢ ( 𝜑 → ( +∞ ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) = +∞ ) )
22 21 adantr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → ( +∞ ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) = +∞ ) )
23 18 22 mpbid ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → ∃ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) = +∞ )
24 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
25 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐺 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
26 24 25 sselid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ* )
27 26 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = +∞ ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ* )
28 id ⊢ ( ( 𝐹 ‘ 𝑥 ) = +∞ → ( 𝐹 ‘ 𝑥 ) = +∞ )
29 28 eqcomd ⊢ ( ( 𝐹 ‘ 𝑥 ) = +∞ → +∞ = ( 𝐹 ‘ 𝑥 ) )
30 29 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = +∞ ) → +∞ = ( 𝐹 ‘ 𝑥 ) )
31 4 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = +∞ ) → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) )
32 30 31 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = +∞ ) → +∞ ≤ ( 𝐺 ‘ 𝑥 ) )
33 27 32 xrgepnfd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = +∞ ) → ( 𝐺 ‘ 𝑥 ) = +∞ )
34 33 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = +∞ ) → +∞ = ( 𝐺 ‘ 𝑥 ) )
35 3 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝑋 )
36 35 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐺 Fn 𝑋 )
37 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
38 fnfvelrn ⊢ ( ( 𝐺 Fn 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐺 ‘ 𝑥 ) ∈ ran 𝐺 )
39 36 37 38 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐺 ‘ 𝑥 ) ∈ ran 𝐺 )
40 39 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = +∞ ) → ( 𝐺 ‘ 𝑥 ) ∈ ran 𝐺 )
41 34 40 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = +∞ ) → +∞ ∈ ran 𝐺 )
42 41 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) = +∞ → +∞ ∈ ran 𝐺 ) )
43 42 adantlr ⊢ ( ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) = +∞ → +∞ ∈ ran 𝐺 ) )
44 43 rexlimdva ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → ( ∃ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) = +∞ → +∞ ∈ ran 𝐺 ) )
45 23 44 mpd ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → +∞ ∈ ran 𝐺 )
46 16 17 45 sge0pnfval ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → ( Σ^ ‘ 𝐺 ) = +∞ )
47 46 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) ∧ +∞ ∈ ran 𝐹 ) → ( Σ^ ‘ 𝐺 ) = +∞ )
48 simplr ⊢ ( ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) ∧ +∞ ∈ ran 𝐹 ) → ¬ ( Σ^ ‘ 𝐺 ) = +∞ )
49 47 48 pm2.65da ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) → ¬ +∞ ∈ ran 𝐹 )
50 15 49 fge0iccico ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) → 𝐹 : 𝑋 ⟶ ( 0 [,) +∞ ) )
51 50 adantr ⊢ ( ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) ∧ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝐹 : 𝑋 ⟶ ( 0 [,) +∞ ) )
52 elpwinss ⊢ ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑦 ⊆ 𝑋 )
53 52 adantl ⊢ ( ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) ∧ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑦 ⊆ 𝑋 )
54 51 53 fssresd ⊢ ( ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) ∧ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( 0 [,) +∞ ) )
55 14 54 sge0fsum ⊢ ( ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) ∧ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝑦 ) ) = Σ 𝑥 ∈ 𝑦 ( ( 𝐹 ↾ 𝑦 ) ‘ 𝑥 ) )
56 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
57 54 ffvelrnda ⊢ ( ( ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) ∧ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → ( ( 𝐹 ↾ 𝑦 ) ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
58 56 57 sselid ⊢ ( ( ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) ∧ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → ( ( 𝐹 ↾ 𝑦 ) ‘ 𝑥 ) ∈ ℝ )
59 14 58 fsumrecl ⊢ ( ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) ∧ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → Σ 𝑥 ∈ 𝑦 ( ( 𝐹 ↾ 𝑦 ) ‘ 𝑥 ) ∈ ℝ )
60 55 59 eqeltrd ⊢ ( ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) ∧ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝑦 ) ) ∈ ℝ )
61 3 adantr ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) → 𝐺 : 𝑋 ⟶ ( 0 [,] +∞ ) )
62 1 adantr ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) → 𝑋 ∈ 𝑉 )
63 simpr ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) → ¬ ( Σ^ ‘ 𝐺 ) = +∞ )
64 62 61 sge0repnf ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) → ( ( Σ^ ‘ 𝐺 ) ∈ ℝ ↔ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) )
65 63 64 mpbird ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) → ( Σ^ ‘ 𝐺 ) ∈ ℝ )
66 62 61 65 sge0rern ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) → ¬ +∞ ∈ ran 𝐺 )
67 61 66 fge0iccico ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) → 𝐺 : 𝑋 ⟶ ( 0 [,) +∞ ) )
68 67 adantr ⊢ ( ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) ∧ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝐺 : 𝑋 ⟶ ( 0 [,) +∞ ) )
69 68 53 fssresd ⊢ ( ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) ∧ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( 𝐺 ↾ 𝑦 ) : 𝑦 ⟶ ( 0 [,) +∞ ) )
70 14 69 sge0fsum ⊢ ( ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) ∧ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( Σ^ ‘ ( 𝐺 ↾ 𝑦 ) ) = Σ 𝑥 ∈ 𝑦 ( ( 𝐺 ↾ 𝑦 ) ‘ 𝑥 ) )
71 69 ffvelrnda ⊢ ( ( ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) ∧ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → ( ( 𝐺 ↾ 𝑦 ) ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
72 56 71 sselid ⊢ ( ( ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) ∧ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → ( ( 𝐺 ↾ 𝑦 ) ‘ 𝑥 ) ∈ ℝ )
73 14 72 fsumrecl ⊢ ( ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) ∧ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → Σ 𝑥 ∈ 𝑦 ( ( 𝐺 ↾ 𝑦 ) ‘ 𝑥 ) ∈ ℝ )
74 70 73 eqeltrd ⊢ ( ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) ∧ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( Σ^ ‘ ( 𝐺 ↾ 𝑦 ) ) ∈ ℝ )
75 65 adantr ⊢ ( ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) ∧ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( Σ^ ‘ 𝐺 ) ∈ ℝ )
76 simplll ⊢ ( ( ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) ∧ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → 𝜑 )
77 53 sselda ⊢ ( ( ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) ∧ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → 𝑥 ∈ 𝑋 )
78 76 77 4 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) ∧ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) )
79 fvres ⊢ ( 𝑥 ∈ 𝑦 → ( ( 𝐹 ↾ 𝑦 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
80 79 adantl ⊢ ( ( ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) ∧ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → ( ( 𝐹 ↾ 𝑦 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
81 fvres ⊢ ( 𝑥 ∈ 𝑦 → ( ( 𝐺 ↾ 𝑦 ) ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
82 81 adantl ⊢ ( ( ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) ∧ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → ( ( 𝐺 ↾ 𝑦 ) ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
83 80 82 breq12d ⊢ ( ( ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) ∧ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → ( ( ( 𝐹 ↾ 𝑦 ) ‘ 𝑥 ) ≤ ( ( 𝐺 ↾ 𝑦 ) ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) ) )
84 78 83 mpbird ⊢ ( ( ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) ∧ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑦 ) → ( ( 𝐹 ↾ 𝑦 ) ‘ 𝑥 ) ≤ ( ( 𝐺 ↾ 𝑦 ) ‘ 𝑥 ) )
85 14 58 72 84 fsumle ⊢ ( ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) ∧ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → Σ 𝑥 ∈ 𝑦 ( ( 𝐹 ↾ 𝑦 ) ‘ 𝑥 ) ≤ Σ 𝑥 ∈ 𝑦 ( ( 𝐺 ↾ 𝑦 ) ‘ 𝑥 ) )
86 55 70 breq12d ⊢ ( ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) ∧ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( ( Σ^ ‘ ( 𝐹 ↾ 𝑦 ) ) ≤ ( Σ^ ‘ ( 𝐺 ↾ 𝑦 ) ) ↔ Σ 𝑥 ∈ 𝑦 ( ( 𝐹 ↾ 𝑦 ) ‘ 𝑥 ) ≤ Σ 𝑥 ∈ 𝑦 ( ( 𝐺 ↾ 𝑦 ) ‘ 𝑥 ) ) )
87 85 86 mpbird ⊢ ( ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) ∧ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝑦 ) ) ≤ ( Σ^ ‘ ( 𝐺 ↾ 𝑦 ) ) )
88 1 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑋 ∈ 𝑉 )
89 3 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝐺 : 𝑋 ⟶ ( 0 [,] +∞ ) )
90 88 89 sge0less ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( Σ^ ‘ ( 𝐺 ↾ 𝑦 ) ) ≤ ( Σ^ ‘ 𝐺 ) )
91 90 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) ∧ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( Σ^ ‘ ( 𝐺 ↾ 𝑦 ) ) ≤ ( Σ^ ‘ 𝐺 ) )
92 60 74 75 87 91 letrd ⊢ ( ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) ∧ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝑦 ) ) ≤ ( Σ^ ‘ 𝐺 ) )
93 92 ralrimiva ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) → ∀ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑦 ) ) ≤ ( Σ^ ‘ 𝐺 ) )
94 62 61 sge0xrcl ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) → ( Σ^ ‘ 𝐺 ) ∈ ℝ* )
95 62 15 94 sge0lefi ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) → ( ( Σ^ ‘ 𝐹 ) ≤ ( Σ^ ‘ 𝐺 ) ↔ ∀ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑦 ) ) ≤ ( Σ^ ‘ 𝐺 ) ) )
96 93 95 mpbird ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐺 ) = +∞ ) → ( Σ^ ‘ 𝐹 ) ≤ ( Σ^ ‘ 𝐺 ) )
97 12 96 pm2.61dan ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ≤ ( Σ^ ‘ 𝐺 ) )