Metamath Proof Explorer

Theorem sge0cl

Description: The arbitrary sum of nonnegative extended reals is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0cl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
sge0cl.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
Assertion sge0cl ( 𝜑 → ( Σ^ ‘ 𝐹 ) ∈ ( 0 [,] +∞ ) )

Proof

Step Hyp Ref Expression
1 sge0cl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2 sge0cl.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
3 fveq2 ⊢ ( 𝐹 = ∅ → ( Σ^ ‘ 𝐹 ) = ( Σ^ ‘ ∅ ) )
4 sge00 ⊢ ( Σ^ ‘ ∅ ) = 0
5 4 a1i ⊢ ( 𝐹 = ∅ → ( Σ^ ‘ ∅ ) = 0 )
6 3 5 eqtrd ⊢ ( 𝐹 = ∅ → ( Σ^ ‘ 𝐹 ) = 0 )
7 0e0iccpnf ⊢ 0 ∈ ( 0 [,] +∞ )
8 7 a1i ⊢ ( 𝐹 = ∅ → 0 ∈ ( 0 [,] +∞ ) )
9 6 8 eqeltrd ⊢ ( 𝐹 = ∅ → ( Σ^ ‘ 𝐹 ) ∈ ( 0 [,] +∞ ) )
10 9 adantl ⊢ ( ( 𝜑 ∧ 𝐹 = ∅ ) → ( Σ^ ‘ 𝐹 ) ∈ ( 0 [,] +∞ ) )
11 1 adantr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → 𝑋 ∈ 𝑉 )
12 2 adantr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
13 simpr ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → +∞ ∈ ran 𝐹 )
14 11 12 13 sge0pnfval ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → ( Σ^ ‘ 𝐹 ) = +∞ )
15 pnfel0pnf ⊢ +∞ ∈ ( 0 [,] +∞ )
16 15 a1i ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → +∞ ∈ ( 0 [,] +∞ ) )
17 14 16 eqeltrd ⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → ( Σ^ ‘ 𝐹 ) ∈ ( 0 [,] +∞ ) )
18 17 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐹 = ∅ ) ∧ +∞ ∈ ran 𝐹 ) → ( Σ^ ‘ 𝐹 ) ∈ ( 0 [,] +∞ ) )
19 simpll ⊢ ( ( ( 𝜑 ∧ ¬ 𝐹 = ∅ ) ∧ ¬ +∞ ∈ ran 𝐹 ) → 𝜑 )
20 neqne ⊢ ( ¬ 𝐹 = ∅ → 𝐹 ≠ ∅ )
21 20 ad2antlr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐹 = ∅ ) ∧ ¬ +∞ ∈ ran 𝐹 ) → 𝐹 ≠ ∅ )
22 simpr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐹 = ∅ ) ∧ ¬ +∞ ∈ ran 𝐹 ) → ¬ +∞ ∈ ran 𝐹 )
23 0xr ⊢ 0 ∈ ℝ*
24 23 a1i ⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ∅ ) ∧ ¬ +∞ ∈ ran 𝐹 ) → 0 ∈ ℝ* )
25 pnfxr ⊢ +∞ ∈ ℝ*
26 25 a1i ⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ∅ ) ∧ ¬ +∞ ∈ ran 𝐹 ) → +∞ ∈ ℝ* )
27 1 adantr ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) → 𝑋 ∈ 𝑉 )
28 2 adantr ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
29 simpr ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) → ¬ +∞ ∈ ran 𝐹 )
30 28 29 fge0iccico ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) → 𝐹 : 𝑋 ⟶ ( 0 [,) +∞ ) )
31 27 30 sge0reval ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) → ( Σ^ ‘ 𝐹 ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) )
32 elinel2 ⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑥 ∈ Fin )
33 32 adantl ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑥 ∈ Fin )
34 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
35 elinel1 ⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑥 ∈ 𝒫 𝑋 )
36 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝑋 → 𝑥 ⊆ 𝑋 )
37 35 36 syl ⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑥 ⊆ 𝑋 )
38 37 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑥 ⊆ 𝑋 )
39 38 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑥 ⊆ 𝑋 )
40 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑥 )
41 39 40 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑋 )
42 34 41 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) )
43 42 adantllr ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) )
44 nne ⊢ ( ¬ ( 𝐹 ‘ 𝑦 ) ≠ +∞ ↔ ( 𝐹 ‘ 𝑦 ) = +∞ )
45 44 biimpi ⊢ ( ¬ ( 𝐹 ‘ 𝑦 ) ≠ +∞ → ( 𝐹 ‘ 𝑦 ) = +∞ )
46 45 eqcomd ⊢ ( ¬ ( 𝐹 ‘ 𝑦 ) ≠ +∞ → +∞ = ( 𝐹 ‘ 𝑦 ) )
47 46 adantl ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ ( 𝐹 ‘ 𝑦 ) ≠ +∞ ) → +∞ = ( 𝐹 ‘ 𝑦 ) )
48 2 ffund ⊢ ( 𝜑 → Fun 𝐹 )
49 48 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → Fun 𝐹 )
50 41 3impa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑋 )
51 2 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝑋 )
52 51 eqcomd ⊢ ( 𝜑 → 𝑋 = dom 𝐹 )
53 52 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → 𝑋 = dom 𝐹 )
54 50 53 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ dom 𝐹 )
55 fvelrn ⊢ ( ( Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑦 ) ∈ ran 𝐹 )
56 49 54 55 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ∈ ran 𝐹 )
57 56 ad5ant134 ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ ( 𝐹 ‘ 𝑦 ) ≠ +∞ ) → ( 𝐹 ‘ 𝑦 ) ∈ ran 𝐹 )
58 47 57 eqeltrd ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ ( 𝐹 ‘ 𝑦 ) ≠ +∞ ) → +∞ ∈ ran 𝐹 )
59 29 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ ( 𝐹 ‘ 𝑦 ) ≠ +∞ ) → ¬ +∞ ∈ ran 𝐹 )
60 58 59 condan ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ≠ +∞ )
61 ge0xrre ⊢ ( ( ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) ∧ ( 𝐹 ‘ 𝑦 ) ≠ +∞ ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
62 43 60 61 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
63 33 62 fsumrecl ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
64 63 ralrimiva ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) → ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
65 eqid ⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) = ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
66 65 rnmptss ⊢ ( ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ℝ → ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ⊆ ℝ )
67 64 66 syl ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) → ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ⊆ ℝ )
68 ressxr ⊢ ℝ ⊆ ℝ*
69 68 a1i ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) → ℝ ⊆ ℝ* )
70 67 69 sstrd ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) → ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ⊆ ℝ* )
71 supxrcl ⊢ ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ⊆ ℝ* → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) ∈ ℝ* )
72 70 71 syl ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) ∈ ℝ* )
73 31 72 eqeltrd ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) → ( Σ^ ‘ 𝐹 ) ∈ ℝ* )
74 73 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ∅ ) ∧ ¬ +∞ ∈ ran 𝐹 ) → ( Σ^ ‘ 𝐹 ) ∈ ℝ* )
75 52 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ≠ ∅ ) → 𝑋 = dom 𝐹 )
76 neneq ⊢ ( 𝐹 ≠ ∅ → ¬ 𝐹 = ∅ )
77 76 adantl ⊢ ( ( 𝜑 ∧ 𝐹 ≠ ∅ ) → ¬ 𝐹 = ∅ )
78 frel ⊢ ( 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) → Rel 𝐹 )
79 2 78 syl ⊢ ( 𝜑 → Rel 𝐹 )
80 79 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ≠ ∅ ) → Rel 𝐹 )
81 reldm0 ⊢ ( Rel 𝐹 → ( 𝐹 = ∅ ↔ dom 𝐹 = ∅ ) )
82 80 81 syl ⊢ ( ( 𝜑 ∧ 𝐹 ≠ ∅ ) → ( 𝐹 = ∅ ↔ dom 𝐹 = ∅ ) )
83 77 82 mtbid ⊢ ( ( 𝜑 ∧ 𝐹 ≠ ∅ ) → ¬ dom 𝐹 = ∅ )
84 83 neqned ⊢ ( ( 𝜑 ∧ 𝐹 ≠ ∅ ) → dom 𝐹 ≠ ∅ )
85 75 84 eqnetrd ⊢ ( ( 𝜑 ∧ 𝐹 ≠ ∅ ) → 𝑋 ≠ ∅ )
86 n0 ⊢ ( 𝑋 ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ 𝑋 )
87 85 86 sylib ⊢ ( ( 𝜑 ∧ 𝐹 ≠ ∅ ) → ∃ 𝑧 𝑧 ∈ 𝑋 )
88 87 adantr ⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ∅ ) ∧ ¬ +∞ ∈ ran 𝐹 ) → ∃ 𝑧 𝑧 ∈ 𝑋 )
89 23 a1i ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝑋 ) → 0 ∈ ℝ* )
90 2 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑧 ) ∈ ( 0 [,] +∞ ) )
91 90 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑧 ) ∈ ( 0 [,] +∞ ) )
92 nne ⊢ ( ¬ ( 𝐹 ‘ 𝑧 ) ≠ +∞ ↔ ( 𝐹 ‘ 𝑧 ) = +∞ )
93 92 biimpi ⊢ ( ¬ ( 𝐹 ‘ 𝑧 ) ≠ +∞ → ( 𝐹 ‘ 𝑧 ) = +∞ )
94 93 eqcomd ⊢ ( ¬ ( 𝐹 ‘ 𝑧 ) ≠ +∞ → +∞ = ( 𝐹 ‘ 𝑧 ) )
95 94 adantl ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝑋 ) ∧ ¬ ( 𝐹 ‘ 𝑧 ) ≠ +∞ ) → +∞ = ( 𝐹 ‘ 𝑧 ) )
96 2 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
97 96 ffund ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → Fun 𝐹 )
98 simpr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ∈ 𝑋 )
99 52 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → 𝑋 = dom 𝐹 )
100 98 99 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ∈ dom 𝐹 )
101 fvelrn ⊢ ( ( Fun 𝐹 ∧ 𝑧 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑧 ) ∈ ran 𝐹 )
102 97 100 101 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑧 ) ∈ ran 𝐹 )
103 102 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑧 ) ∈ ran 𝐹 )
104 103 adantr ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝑋 ) ∧ ¬ ( 𝐹 ‘ 𝑧 ) ≠ +∞ ) → ( 𝐹 ‘ 𝑧 ) ∈ ran 𝐹 )
105 95 104 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝑋 ) ∧ ¬ ( 𝐹 ‘ 𝑧 ) ≠ +∞ ) → +∞ ∈ ran 𝐹 )
106 29 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝑋 ) ∧ ¬ ( 𝐹 ‘ 𝑧 ) ≠ +∞ ) → ¬ +∞ ∈ ran 𝐹 )
107 105 106 condan ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑧 ) ≠ +∞ )
108 ge0xrre ⊢ ( ( ( 𝐹 ‘ 𝑧 ) ∈ ( 0 [,] +∞ ) ∧ ( 𝐹 ‘ 𝑧 ) ≠ +∞ ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
109 91 107 108 syl2anc ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
110 109 rexrd ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ* )
111 73 adantr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝑋 ) → ( Σ^ ‘ 𝐹 ) ∈ ℝ* )
112 23 a1i ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → 0 ∈ ℝ* )
113 25 a1i ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → +∞ ∈ ℝ* )
114 iccgelb ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( 0 [,] +∞ ) ) → 0 ≤ ( 𝐹 ‘ 𝑧 ) )
115 112 113 90 114 syl3anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → 0 ≤ ( 𝐹 ‘ 𝑧 ) )
116 115 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝑋 ) → 0 ≤ ( 𝐹 ‘ 𝑧 ) )
117 70 adantr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝑋 ) → ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ⊆ ℝ* )
118 snelpwi ⊢ ( 𝑧 ∈ 𝑋 → { 𝑧 } ∈ 𝒫 𝑋 )
119 snfi ⊢ { 𝑧 } ∈ Fin
120 119 a1i ⊢ ( 𝑧 ∈ 𝑋 → { 𝑧 } ∈ Fin )
121 118 120 elind ⊢ ( 𝑧 ∈ 𝑋 → { 𝑧 } ∈ ( 𝒫 𝑋 ∩ Fin ) )
122 121 adantl ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝑋 ) → { 𝑧 } ∈ ( 𝒫 𝑋 ∩ Fin ) )
123 simpr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ∈ 𝑋 )
124 109 recnd ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
125 fveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) )
126 125 sumsn ⊢ ( ( 𝑧 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℂ ) → Σ 𝑦 ∈ { 𝑧 } ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) )
127 123 124 126 syl2anc ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝑋 ) → Σ 𝑦 ∈ { 𝑧 } ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) )
128 127 eqcomd ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑧 ) = Σ 𝑦 ∈ { 𝑧 } ( 𝐹 ‘ 𝑦 ) )
129 sumeq1 ⊢ ( 𝑥 = { 𝑧 } → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = Σ 𝑦 ∈ { 𝑧 } ( 𝐹 ‘ 𝑦 ) )
130 129 rspceeqv ⊢ ( ( { 𝑧 } ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ( 𝐹 ‘ 𝑧 ) = Σ 𝑦 ∈ { 𝑧 } ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( 𝐹 ‘ 𝑧 ) = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
131 122 128 130 syl2anc ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝑋 ) → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( 𝐹 ‘ 𝑧 ) = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
132 65 elrnmpt ⊢ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 0 [,] +∞ ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( 𝐹 ‘ 𝑧 ) = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
133 91 132 syl ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( 𝐹 ‘ 𝑧 ) = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
134 131 133 mpbird ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑧 ) ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
135 supxrub ⊢ ( ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ⊆ ℝ* ∧ ( 𝐹 ‘ 𝑧 ) ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐹 ‘ 𝑧 ) ≤ sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) )
136 117 134 135 syl2anc ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑧 ) ≤ sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) )
137 31 eqcomd ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) = ( Σ^ ‘ 𝐹 ) )
138 137 adantr ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝑋 ) → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) = ( Σ^ ‘ 𝐹 ) )
139 136 138 breqtrd ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑧 ) ≤ ( Σ^ ‘ 𝐹 ) )
140 89 110 111 116 139 xrletrd ⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝑋 ) → 0 ≤ ( Σ^ ‘ 𝐹 ) )
141 140 ex ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) → ( 𝑧 ∈ 𝑋 → 0 ≤ ( Σ^ ‘ 𝐹 ) ) )
142 141 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ∅ ) ∧ ¬ +∞ ∈ ran 𝐹 ) → ( 𝑧 ∈ 𝑋 → 0 ≤ ( Σ^ ‘ 𝐹 ) ) )
143 142 exlimdv ⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ∅ ) ∧ ¬ +∞ ∈ ran 𝐹 ) → ( ∃ 𝑧 𝑧 ∈ 𝑋 → 0 ≤ ( Σ^ ‘ 𝐹 ) ) )
144 88 143 mpd ⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ∅ ) ∧ ¬ +∞ ∈ ran 𝐹 ) → 0 ≤ ( Σ^ ‘ 𝐹 ) )
145 pnfge ⊢ ( ( Σ^ ‘ 𝐹 ) ∈ ℝ* → ( Σ^ ‘ 𝐹 ) ≤ +∞ )
146 73 145 syl ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran 𝐹 ) → ( Σ^ ‘ 𝐹 ) ≤ +∞ )
147 146 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ∅ ) ∧ ¬ +∞ ∈ ran 𝐹 ) → ( Σ^ ‘ 𝐹 ) ≤ +∞ )
148 24 26 74 144 147 eliccxrd ⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ∅ ) ∧ ¬ +∞ ∈ ran 𝐹 ) → ( Σ^ ‘ 𝐹 ) ∈ ( 0 [,] +∞ ) )
149 19 21 22 148 syl21anc ⊢ ( ( ( 𝜑 ∧ ¬ 𝐹 = ∅ ) ∧ ¬ +∞ ∈ ran 𝐹 ) → ( Σ^ ‘ 𝐹 ) ∈ ( 0 [,] +∞ ) )
150 18 149 pm2.61dan ⊢ ( ( 𝜑 ∧ ¬ 𝐹 = ∅ ) → ( Σ^ ‘ 𝐹 ) ∈ ( 0 [,] +∞ ) )
151 10 150 pm2.61dan ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ∈ ( 0 [,] +∞ ) )