# 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 ${⊢}{\phi }\to {X}\in {V}$
sge0cl.f ${⊢}{\phi }\to {F}:{X}⟶\left[0,\mathrm{+\infty }\right]$
Assertion sge0cl ${⊢}{\phi }\to \mathrm{sum^}\left({F}\right)\in \left[0,\mathrm{+\infty }\right]$

### Proof

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