Metamath Proof Explorer

Theorem xrge0tsms

Description: Any finite or infinite sum in the nonnegative extended reals is uniquely convergent to the supremum of all finite sums. (Contributed by Mario Carneiro, 13-Sep-2015) (Proof shortened by AV, 26-Jul-2019)

Ref Expression
Hypotheses xrge0tsms.g 
|- G = ( RR*s |`s ( 0 [,] +oo ) )
xrge0tsms.a 
|- ( ph -> A e. V )
xrge0tsms.f 
|- ( ph -> F : A --> ( 0 [,] +oo ) )
xrge0tsms.s 
|- S = sup ( ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) , RR* , < )
Assertion xrge0tsms 
|- ( ph -> ( G tsums F ) = { S } )

Proof

Step Hyp Ref Expression
1 xrge0tsms.g 
 |-  G = ( RR*s |`s ( 0 [,] +oo ) )
2 xrge0tsms.a 
 |-  ( ph -> A e. V )
3 xrge0tsms.f 
 |-  ( ph -> F : A --> ( 0 [,] +oo ) )
4 xrge0tsms.s 
 |-  S = sup ( ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) , RR* , < )
5 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
6 xrsbas 
 |-  RR* = ( Base ` RR*s )
7 1 6 ressbas2 
 |-  ( ( 0 [,] +oo ) C_ RR* -> ( 0 [,] +oo ) = ( Base ` G ) )
8 5 7 ax-mp 
 |-  ( 0 [,] +oo ) = ( Base ` G )
9 eqid 
 |-  ( RR*s |`s ( RR* \ { -oo } ) ) = ( RR*s |`s ( RR* \ { -oo } ) )
10 9 xrge0subm 
 |-  ( 0 [,] +oo ) e. ( SubMnd ` ( RR*s |`s ( RR* \ { -oo } ) ) )
11 xrex 
 |-  RR* e. _V
12 11 difexi 
 |-  ( RR* \ { -oo } ) e. _V
13 simpl 
 |-  ( ( x e. RR* /\ 0 <_ x ) -> x e. RR* )
14 ge0nemnf 
 |-  ( ( x e. RR* /\ 0 <_ x ) -> x =/= -oo )
15 13 14 jca 
 |-  ( ( x e. RR* /\ 0 <_ x ) -> ( x e. RR* /\ x =/= -oo ) )
16 elxrge0 
 |-  ( x e. ( 0 [,] +oo ) <-> ( x e. RR* /\ 0 <_ x ) )
17 eldifsn 
 |-  ( x e. ( RR* \ { -oo } ) <-> ( x e. RR* /\ x =/= -oo ) )
18 15 16 17 3imtr4i 
 |-  ( x e. ( 0 [,] +oo ) -> x e. ( RR* \ { -oo } ) )
19 18 ssriv 
 |-  ( 0 [,] +oo ) C_ ( RR* \ { -oo } )
20 ressabs 
 |-  ( ( ( RR* \ { -oo } ) e. _V /\ ( 0 [,] +oo ) C_ ( RR* \ { -oo } ) ) -> ( ( RR*s |`s ( RR* \ { -oo } ) ) |`s ( 0 [,] +oo ) ) = ( RR*s |`s ( 0 [,] +oo ) ) )
21 12 19 20 mp2an 
 |-  ( ( RR*s |`s ( RR* \ { -oo } ) ) |`s ( 0 [,] +oo ) ) = ( RR*s |`s ( 0 [,] +oo ) )
22 1 21 eqtr4i 
 |-  G = ( ( RR*s |`s ( RR* \ { -oo } ) ) |`s ( 0 [,] +oo ) )
23 9 xrs10 
 |-  0 = ( 0g ` ( RR*s |`s ( RR* \ { -oo } ) ) )
24 22 23 subm0 
 |-  ( ( 0 [,] +oo ) e. ( SubMnd ` ( RR*s |`s ( RR* \ { -oo } ) ) ) -> 0 = ( 0g ` G ) )
25 10 24 ax-mp 
 |-  0 = ( 0g ` G )
26 xrge0cmn 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd
27 1 26 eqeltri 
 |-  G e. CMnd
28 27 a1i 
 |-  ( ( ph /\ s e. ( ~P A i^i Fin ) ) -> G e. CMnd )
29 elinel2 
 |-  ( s e. ( ~P A i^i Fin ) -> s e. Fin )
30 29 adantl 
 |-  ( ( ph /\ s e. ( ~P A i^i Fin ) ) -> s e. Fin )
31 elfpw 
 |-  ( s e. ( ~P A i^i Fin ) <-> ( s C_ A /\ s e. Fin ) )
32 31 simplbi 
 |-  ( s e. ( ~P A i^i Fin ) -> s C_ A )
33 fssres 
 |-  ( ( F : A --> ( 0 [,] +oo ) /\ s C_ A ) -> ( F |` s ) : s --> ( 0 [,] +oo ) )
34 3 32 33 syl2an 
 |-  ( ( ph /\ s e. ( ~P A i^i Fin ) ) -> ( F |` s ) : s --> ( 0 [,] +oo ) )
35 c0ex 
 |-  0 e. _V
36 35 a1i 
 |-  ( ( ph /\ s e. ( ~P A i^i Fin ) ) -> 0 e. _V )
37 34 30 36 fdmfifsupp 
 |-  ( ( ph /\ s e. ( ~P A i^i Fin ) ) -> ( F |` s ) finSupp 0 )
38 8 25 28 30 34 37 gsumcl 
 |-  ( ( ph /\ s e. ( ~P A i^i Fin ) ) -> ( G gsum ( F |` s ) ) e. ( 0 [,] +oo ) )
39 5 38 sselid 
 |-  ( ( ph /\ s e. ( ~P A i^i Fin ) ) -> ( G gsum ( F |` s ) ) e. RR* )
40 39 fmpttd 
 |-  ( ph -> ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) : ( ~P A i^i Fin ) --> RR* )
41 40 frnd 
 |-  ( ph -> ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) C_ RR* )
42 supxrcl 
 |-  ( ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) C_ RR* -> sup ( ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) , RR* , < ) e. RR* )
43 41 42 syl 
 |-  ( ph -> sup ( ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) , RR* , < ) e. RR* )
44 4 43 eqeltrid 
 |-  ( ph -> S e. RR* )
45 0ss 
 |-  (/) C_ A
46 0fi 
 |-  (/) e. Fin
47 elfpw 
 |-  ( (/) e. ( ~P A i^i Fin ) <-> ( (/) C_ A /\ (/) e. Fin ) )
48 45 46 47 mpbir2an 
 |-  (/) e. ( ~P A i^i Fin )
49 0cn 
 |-  0 e. CC
50 eqid 
 |-  ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) = ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) )
51 reseq2 
 |-  ( s = (/) -> ( F |` s ) = ( F |` (/) ) )
52 res0 
 |-  ( F |` (/) ) = (/)
53 51 52 eqtrdi 
 |-  ( s = (/) -> ( F |` s ) = (/) )
54 53 oveq2d 
 |-  ( s = (/) -> ( G gsum ( F |` s ) ) = ( G gsum (/) ) )
55 25 gsum0 
 |-  ( G gsum (/) ) = 0
56 54 55 eqtrdi 
 |-  ( s = (/) -> ( G gsum ( F |` s ) ) = 0 )
57 50 56 elrnmpt1s 
 |-  ( ( (/) e. ( ~P A i^i Fin ) /\ 0 e. CC ) -> 0 e. ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) )
58 48 49 57 mp2an 
 |-  0 e. ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) )
59 supxrub 
 |-  ( ( ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) C_ RR* /\ 0 e. ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) ) -> 0 <_ sup ( ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) , RR* , < ) )
60 41 58 59 sylancl 
 |-  ( ph -> 0 <_ sup ( ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) , RR* , < ) )
61 60 4 breqtrrdi 
 |-  ( ph -> 0 <_ S )
62 elxrge0 
 |-  ( S e. ( 0 [,] +oo ) <-> ( S e. RR* /\ 0 <_ S ) )
63 44 61 62 sylanbrc 
 |-  ( ph -> S e. ( 0 [,] +oo ) )
64 letop 
 |-  ( ordTop ` <_ ) e. Top
65 ovex 
 |-  ( 0 [,] +oo ) e. _V
66 elrest 
 |-  ( ( ( ordTop ` <_ ) e. Top /\ ( 0 [,] +oo ) e. _V ) -> ( u e. ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) <-> E. v e. ( ordTop ` <_ ) u = ( v i^i ( 0 [,] +oo ) ) ) )
67 64 65 66 mp2an 
 |-  ( u e. ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) <-> E. v e. ( ordTop ` <_ ) u = ( v i^i ( 0 [,] +oo ) ) )
68 elinel1 
 |-  ( S e. ( v i^i ( 0 [,] +oo ) ) -> S e. v )
69 reex 
 |-  RR e. _V
70 simplrl 
 |-  ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) -> v e. ( ordTop ` <_ ) )
71 elrestr 
 |-  ( ( ( ordTop ` <_ ) e. Top /\ RR e. _V /\ v e. ( ordTop ` <_ ) ) -> ( v i^i RR ) e. ( ( ordTop ` <_ ) |`t RR ) )
72 64 69 70 71 mp3an12i 
 |-  ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) -> ( v i^i RR ) e. ( ( ordTop ` <_ ) |`t RR ) )
73 eqid 
 |-  ( ( ordTop ` <_ ) |`t RR ) = ( ( ordTop ` <_ ) |`t RR )
74 73 xrtgioo 
 |-  ( topGen ` ran (,) ) = ( ( ordTop ` <_ ) |`t RR )
75 72 74 eleqtrrdi 
 |-  ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) -> ( v i^i RR ) e. ( topGen ` ran (,) ) )
76 simplrr 
 |-  ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) -> S e. v )
77 simpr 
 |-  ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) -> S e. RR )
78 76 77 elind 
 |-  ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) -> S e. ( v i^i RR ) )
79 tg2 
 |-  ( ( ( v i^i RR ) e. ( topGen ` ran (,) ) /\ S e. ( v i^i RR ) ) -> E. u e. ran (,) ( S e. u /\ u C_ ( v i^i RR ) ) )
80 75 78 79 syl2anc 
 |-  ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) -> E. u e. ran (,) ( S e. u /\ u C_ ( v i^i RR ) ) )
81 ioof 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
82 ffn 
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> (,) Fn ( RR* X. RR* ) )
83 ovelrn 
 |-  ( (,) Fn ( RR* X. RR* ) -> ( u e. ran (,) <-> E. r e. RR* E. w e. RR* u = ( r (,) w ) ) )
84 81 82 83 mp2b 
 |-  ( u e. ran (,) <-> E. r e. RR* E. w e. RR* u = ( r (,) w ) )
85 simprrr 
 |-  ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) -> ( r (,) w ) C_ ( v i^i RR ) )
86 85 adantr 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> ( r (,) w ) C_ ( v i^i RR ) )
87 inss1 
 |-  ( v i^i RR ) C_ v
88 86 87 sstrdi 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> ( r (,) w ) C_ v )
89 27 a1i 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> G e. CMnd )
90 simprrl 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> y e. ( ~P A i^i Fin ) )
91 elinel2 
 |-  ( y e. ( ~P A i^i Fin ) -> y e. Fin )
92 90 91 syl 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> y e. Fin )
93 simp-4l 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> ph )
94 93 3 syl 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> F : A --> ( 0 [,] +oo ) )
95 elfpw 
 |-  ( y e. ( ~P A i^i Fin ) <-> ( y C_ A /\ y e. Fin ) )
96 95 simplbi 
 |-  ( y e. ( ~P A i^i Fin ) -> y C_ A )
97 90 96 syl 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> y C_ A )
98 94 97 fssresd 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> ( F |` y ) : y --> ( 0 [,] +oo ) )
99 35 a1i 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> 0 e. _V )
100 98 92 99 fdmfifsupp 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> ( F |` y ) finSupp 0 )
101 8 25 89 92 98 100 gsumcl 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> ( G gsum ( F |` y ) ) e. ( 0 [,] +oo ) )
102 5 101 sselid 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> ( G gsum ( F |` y ) ) e. RR* )
103 simprll 
 |-  ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) -> r e. RR* )
104 103 adantr 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> r e. RR* )
105 simprrr 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> z C_ y )
106 92 105 ssfid 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> z e. Fin )
107 105 97 sstrd 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> z C_ A )
108 94 107 fssresd 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> ( F |` z ) : z --> ( 0 [,] +oo ) )
109 108 106 99 fdmfifsupp 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> ( F |` z ) finSupp 0 )
110 8 25 89 106 108 109 gsumcl 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> ( G gsum ( F |` z ) ) e. ( 0 [,] +oo ) )
111 5 110 sselid 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> ( G gsum ( F |` z ) ) e. RR* )
112 simprlr 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> r < ( G gsum ( F |` z ) ) )
113 93 2 syl 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> A e. V )
114 1 113 94 90 105 xrge0gsumle 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> ( G gsum ( F |` z ) ) <_ ( G gsum ( F |` y ) ) )
115 104 111 102 112 114 xrltletrd 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> r < ( G gsum ( F |` y ) ) )
116 93 44 syl 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> S e. RR* )
117 simprlr 
 |-  ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) -> w e. RR* )
118 117 adantr 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> w e. RR* )
119 93 41 syl 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) C_ RR* )
120 ovex 
 |-  ( G gsum ( F |` y ) ) e. _V
121 reseq2 
 |-  ( s = y -> ( F |` s ) = ( F |` y ) )
122 121 oveq2d 
 |-  ( s = y -> ( G gsum ( F |` s ) ) = ( G gsum ( F |` y ) ) )
123 50 122 elrnmpt1s 
 |-  ( ( y e. ( ~P A i^i Fin ) /\ ( G gsum ( F |` y ) ) e. _V ) -> ( G gsum ( F |` y ) ) e. ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) )
124 90 120 123 sylancl 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> ( G gsum ( F |` y ) ) e. ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) )
125 supxrub 
 |-  ( ( ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) C_ RR* /\ ( G gsum ( F |` y ) ) e. ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) ) -> ( G gsum ( F |` y ) ) <_ sup ( ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) , RR* , < ) )
126 119 124 125 syl2anc 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> ( G gsum ( F |` y ) ) <_ sup ( ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) , RR* , < ) )
127 126 4 breqtrrdi 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> ( G gsum ( F |` y ) ) <_ S )
128 simprrl 
 |-  ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) -> S e. ( r (,) w ) )
129 eliooord 
 |-  ( S e. ( r (,) w ) -> ( r < S /\ S < w ) )
130 128 129 syl 
 |-  ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) -> ( r < S /\ S < w ) )
131 130 simprd 
 |-  ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) -> S < w )
132 131 adantr 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> S < w )
133 102 116 118 127 132 xrlelttrd 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> ( G gsum ( F |` y ) ) < w )
134 elioo1 
 |-  ( ( r e. RR* /\ w e. RR* ) -> ( ( G gsum ( F |` y ) ) e. ( r (,) w ) <-> ( ( G gsum ( F |` y ) ) e. RR* /\ r < ( G gsum ( F |` y ) ) /\ ( G gsum ( F |` y ) ) < w ) ) )
135 104 118 134 syl2anc 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> ( ( G gsum ( F |` y ) ) e. ( r (,) w ) <-> ( ( G gsum ( F |` y ) ) e. RR* /\ r < ( G gsum ( F |` y ) ) /\ ( G gsum ( F |` y ) ) < w ) ) )
136 102 115 133 135 mpbir3and 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> ( G gsum ( F |` y ) ) e. ( r (,) w ) )
137 88 136 sseldd 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> ( G gsum ( F |` y ) ) e. v )
138 137 101 elind 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) ) -> ( G gsum ( F |` y ) ) e. ( v i^i ( 0 [,] +oo ) ) )
139 138 anassrs 
 |-  ( ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) -> ( G gsum ( F |` y ) ) e. ( v i^i ( 0 [,] +oo ) ) )
140 139 expr 
 |-  ( ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) /\ y e. ( ~P A i^i Fin ) ) -> ( z C_ y -> ( G gsum ( F |` y ) ) e. ( v i^i ( 0 [,] +oo ) ) ) )
141 140 ralrimiva 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) -> A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. ( v i^i ( 0 [,] +oo ) ) ) )
142 130 simpld 
 |-  ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) -> r < S )
143 142 4 breqtrdi 
 |-  ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) -> r < sup ( ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) , RR* , < ) )
144 41 ad3antrrr 
 |-  ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) -> ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) C_ RR* )
145 supxrlub 
 |-  ( ( ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) C_ RR* /\ r e. RR* ) -> ( r < sup ( ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) , RR* , < ) <-> E. w e. ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) r < w ) )
146 144 103 145 syl2anc 
 |-  ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) -> ( r < sup ( ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) , RR* , < ) <-> E. w e. ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) r < w ) )
147 143 146 mpbid 
 |-  ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) -> E. w e. ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) r < w )
148 ovex 
 |-  ( G gsum ( F |` z ) ) e. _V
149 148 rgenw 
 |-  A. z e. ( ~P A i^i Fin ) ( G gsum ( F |` z ) ) e. _V
150 reseq2 
 |-  ( s = z -> ( F |` s ) = ( F |` z ) )
151 150 oveq2d 
 |-  ( s = z -> ( G gsum ( F |` s ) ) = ( G gsum ( F |` z ) ) )
152 151 cbvmptv 
 |-  ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) = ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` z ) ) )
153 breq2 
 |-  ( w = ( G gsum ( F |` z ) ) -> ( r < w <-> r < ( G gsum ( F |` z ) ) ) )
154 152 153 rexrnmptw 
 |-  ( A. z e. ( ~P A i^i Fin ) ( G gsum ( F |` z ) ) e. _V -> ( E. w e. ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) r < w <-> E. z e. ( ~P A i^i Fin ) r < ( G gsum ( F |` z ) ) ) )
155 149 154 ax-mp 
 |-  ( E. w e. ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) r < w <-> E. z e. ( ~P A i^i Fin ) r < ( G gsum ( F |` z ) ) )
156 147 155 sylib 
 |-  ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) -> E. z e. ( ~P A i^i Fin ) r < ( G gsum ( F |` z ) ) )
157 141 156 reximddv 
 |-  ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( ( r e. RR* /\ w e. RR* ) /\ ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) ) -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. ( v i^i ( 0 [,] +oo ) ) ) )
158 157 expr 
 |-  ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( r e. RR* /\ w e. RR* ) ) -> ( ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. ( v i^i ( 0 [,] +oo ) ) ) ) )
159 eleq2 
 |-  ( u = ( r (,) w ) -> ( S e. u <-> S e. ( r (,) w ) ) )
160 sseq1 
 |-  ( u = ( r (,) w ) -> ( u C_ ( v i^i RR ) <-> ( r (,) w ) C_ ( v i^i RR ) ) )
161 159 160 anbi12d 
 |-  ( u = ( r (,) w ) -> ( ( S e. u /\ u C_ ( v i^i RR ) ) <-> ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) ) )
162 161 imbi1d 
 |-  ( u = ( r (,) w ) -> ( ( ( S e. u /\ u C_ ( v i^i RR ) ) -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. ( v i^i ( 0 [,] +oo ) ) ) ) <-> ( ( S e. ( r (,) w ) /\ ( r (,) w ) C_ ( v i^i RR ) ) -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. ( v i^i ( 0 [,] +oo ) ) ) ) ) )
163 158 162 syl5ibrcom 
 |-  ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) /\ ( r e. RR* /\ w e. RR* ) ) -> ( u = ( r (,) w ) -> ( ( S e. u /\ u C_ ( v i^i RR ) ) -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. ( v i^i ( 0 [,] +oo ) ) ) ) ) )
164 163 rexlimdvva 
 |-  ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) -> ( E. r e. RR* E. w e. RR* u = ( r (,) w ) -> ( ( S e. u /\ u C_ ( v i^i RR ) ) -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. ( v i^i ( 0 [,] +oo ) ) ) ) ) )
165 84 164 biimtrid 
 |-  ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) -> ( u e. ran (,) -> ( ( S e. u /\ u C_ ( v i^i RR ) ) -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. ( v i^i ( 0 [,] +oo ) ) ) ) ) )
166 165 rexlimdv 
 |-  ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) -> ( E. u e. ran (,) ( S e. u /\ u C_ ( v i^i RR ) ) -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. ( v i^i ( 0 [,] +oo ) ) ) ) )
167 80 166 mpd 
 |-  ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S e. RR ) -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. ( v i^i ( 0 [,] +oo ) ) ) )
168 simplrl 
 |-  ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) -> v e. ( ordTop ` <_ ) )
169 simpr 
 |-  ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) -> S = +oo )
170 simplrr 
 |-  ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) -> S e. v )
171 169 170 eqeltrrd 
 |-  ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) -> +oo e. v )
172 pnfnei 
 |-  ( ( v e. ( ordTop ` <_ ) /\ +oo e. v ) -> E. r e. RR ( r (,] +oo ) C_ v )
173 168 171 172 syl2anc 
 |-  ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) -> E. r e. RR ( r (,] +oo ) C_ v )
174 simprr 
 |-  ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) -> ( r (,] +oo ) C_ v )
175 174 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) -> ( r (,] +oo ) C_ v )
176 27 a1i 
 |-  ( ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) -> G e. CMnd )
177 91 ad2antrl 
 |-  ( ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) -> y e. Fin )
178 simp-5l 
 |-  ( ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) -> ph )
179 178 3 syl 
 |-  ( ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) -> F : A --> ( 0 [,] +oo ) )
180 96 ad2antrl 
 |-  ( ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) -> y C_ A )
181 179 180 fssresd 
 |-  ( ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) -> ( F |` y ) : y --> ( 0 [,] +oo ) )
182 35 a1i 
 |-  ( ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) -> 0 e. _V )
183 181 177 182 fdmfifsupp 
 |-  ( ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) -> ( F |` y ) finSupp 0 )
184 8 25 176 177 181 183 gsumcl 
 |-  ( ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) -> ( G gsum ( F |` y ) ) e. ( 0 [,] +oo ) )
185 5 184 sselid 
 |-  ( ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) -> ( G gsum ( F |` y ) ) e. RR* )
186 rexr 
 |-  ( r e. RR -> r e. RR* )
187 186 ad2antrl 
 |-  ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) -> r e. RR* )
188 187 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) -> r e. RR* )
189 simprr 
 |-  ( ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) -> z C_ y )
190 177 189 ssfid 
 |-  ( ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) -> z e. Fin )
191 189 180 sstrd 
 |-  ( ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) -> z C_ A )
192 179 191 fssresd 
 |-  ( ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) -> ( F |` z ) : z --> ( 0 [,] +oo ) )
193 192 190 182 fdmfifsupp 
 |-  ( ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) -> ( F |` z ) finSupp 0 )
194 8 25 176 190 192 193 gsumcl 
 |-  ( ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) -> ( G gsum ( F |` z ) ) e. ( 0 [,] +oo ) )
195 5 194 sselid 
 |-  ( ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) -> ( G gsum ( F |` z ) ) e. RR* )
196 simplrr 
 |-  ( ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) -> r < ( G gsum ( F |` z ) ) )
197 178 2 syl 
 |-  ( ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) -> A e. V )
198 simprl 
 |-  ( ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) -> y e. ( ~P A i^i Fin ) )
199 1 197 179 198 189 xrge0gsumle 
 |-  ( ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) -> ( G gsum ( F |` z ) ) <_ ( G gsum ( F |` y ) ) )
200 188 195 185 196 199 xrltletrd 
 |-  ( ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) -> r < ( G gsum ( F |` y ) ) )
201 pnfge 
 |-  ( ( G gsum ( F |` y ) ) e. RR* -> ( G gsum ( F |` y ) ) <_ +oo )
202 185 201 syl 
 |-  ( ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) -> ( G gsum ( F |` y ) ) <_ +oo )
203 pnfxr 
 |-  +oo e. RR*
204 elioc1 
 |-  ( ( r e. RR* /\ +oo e. RR* ) -> ( ( G gsum ( F |` y ) ) e. ( r (,] +oo ) <-> ( ( G gsum ( F |` y ) ) e. RR* /\ r < ( G gsum ( F |` y ) ) /\ ( G gsum ( F |` y ) ) <_ +oo ) ) )
205 188 203 204 sylancl 
 |-  ( ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) -> ( ( G gsum ( F |` y ) ) e. ( r (,] +oo ) <-> ( ( G gsum ( F |` y ) ) e. RR* /\ r < ( G gsum ( F |` y ) ) /\ ( G gsum ( F |` y ) ) <_ +oo ) ) )
206 185 200 202 205 mpbir3and 
 |-  ( ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) -> ( G gsum ( F |` y ) ) e. ( r (,] +oo ) )
207 175 206 sseldd 
 |-  ( ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) -> ( G gsum ( F |` y ) ) e. v )
208 207 184 elind 
 |-  ( ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) /\ ( y e. ( ~P A i^i Fin ) /\ z C_ y ) ) -> ( G gsum ( F |` y ) ) e. ( v i^i ( 0 [,] +oo ) ) )
209 208 expr 
 |-  ( ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) /\ y e. ( ~P A i^i Fin ) ) -> ( z C_ y -> ( G gsum ( F |` y ) ) e. ( v i^i ( 0 [,] +oo ) ) ) )
210 209 ralrimiva 
 |-  ( ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) /\ ( z e. ( ~P A i^i Fin ) /\ r < ( G gsum ( F |` z ) ) ) ) -> A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. ( v i^i ( 0 [,] +oo ) ) ) )
211 ltpnf 
 |-  ( r e. RR -> r < +oo )
212 211 ad2antrl 
 |-  ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) -> r < +oo )
213 simplr 
 |-  ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) -> S = +oo )
214 212 213 breqtrrd 
 |-  ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) -> r < S )
215 214 4 breqtrdi 
 |-  ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) -> r < sup ( ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) , RR* , < ) )
216 41 ad3antrrr 
 |-  ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) -> ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) C_ RR* )
217 216 187 145 syl2anc 
 |-  ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) -> ( r < sup ( ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) , RR* , < ) <-> E. w e. ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) r < w ) )
218 215 217 mpbid 
 |-  ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) -> E. w e. ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) r < w )
219 218 155 sylib 
 |-  ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) -> E. z e. ( ~P A i^i Fin ) r < ( G gsum ( F |` z ) ) )
220 210 219 reximddv 
 |-  ( ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) /\ ( r e. RR /\ ( r (,] +oo ) C_ v ) ) -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. ( v i^i ( 0 [,] +oo ) ) ) )
221 173 220 rexlimddv 
 |-  ( ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) /\ S = +oo ) -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. ( v i^i ( 0 [,] +oo ) ) ) )
222 ge0nemnf 
 |-  ( ( S e. RR* /\ 0 <_ S ) -> S =/= -oo )
223 44 61 222 syl2anc 
 |-  ( ph -> S =/= -oo )
224 44 223 jca 
 |-  ( ph -> ( S e. RR* /\ S =/= -oo ) )
225 224 adantr 
 |-  ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) -> ( S e. RR* /\ S =/= -oo ) )
226 xrnemnf 
 |-  ( ( S e. RR* /\ S =/= -oo ) <-> ( S e. RR \/ S = +oo ) )
227 225 226 sylib 
 |-  ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) -> ( S e. RR \/ S = +oo ) )
228 167 221 227 mpjaodan 
 |-  ( ( ph /\ ( v e. ( ordTop ` <_ ) /\ S e. v ) ) -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. ( v i^i ( 0 [,] +oo ) ) ) )
229 228 expr 
 |-  ( ( ph /\ v e. ( ordTop ` <_ ) ) -> ( S e. v -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. ( v i^i ( 0 [,] +oo ) ) ) ) )
230 68 229 syl5 
 |-  ( ( ph /\ v e. ( ordTop ` <_ ) ) -> ( S e. ( v i^i ( 0 [,] +oo ) ) -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. ( v i^i ( 0 [,] +oo ) ) ) ) )
231 eleq2 
 |-  ( u = ( v i^i ( 0 [,] +oo ) ) -> ( S e. u <-> S e. ( v i^i ( 0 [,] +oo ) ) ) )
232 eleq2 
 |-  ( u = ( v i^i ( 0 [,] +oo ) ) -> ( ( G gsum ( F |` y ) ) e. u <-> ( G gsum ( F |` y ) ) e. ( v i^i ( 0 [,] +oo ) ) ) )
233 232 imbi2d 
 |-  ( u = ( v i^i ( 0 [,] +oo ) ) -> ( ( z C_ y -> ( G gsum ( F |` y ) ) e. u ) <-> ( z C_ y -> ( G gsum ( F |` y ) ) e. ( v i^i ( 0 [,] +oo ) ) ) ) )
234 233 rexralbidv 
 |-  ( u = ( v i^i ( 0 [,] +oo ) ) -> ( E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. u ) <-> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. ( v i^i ( 0 [,] +oo ) ) ) ) )
235 231 234 imbi12d 
 |-  ( u = ( v i^i ( 0 [,] +oo ) ) -> ( ( S e. u -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. u ) ) <-> ( S e. ( v i^i ( 0 [,] +oo ) ) -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. ( v i^i ( 0 [,] +oo ) ) ) ) ) )
236 230 235 syl5ibrcom 
 |-  ( ( ph /\ v e. ( ordTop ` <_ ) ) -> ( u = ( v i^i ( 0 [,] +oo ) ) -> ( S e. u -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. u ) ) ) )
237 236 rexlimdva 
 |-  ( ph -> ( E. v e. ( ordTop ` <_ ) u = ( v i^i ( 0 [,] +oo ) ) -> ( S e. u -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. u ) ) ) )
238 67 237 biimtrid 
 |-  ( ph -> ( u e. ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) -> ( S e. u -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. u ) ) ) )
239 238 ralrimiv 
 |-  ( ph -> A. u e. ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) ( S e. u -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. u ) ) )
240 xrstset 
 |-  ( ordTop ` <_ ) = ( TopSet ` RR*s )
241 1 240 resstset 
 |-  ( ( 0 [,] +oo ) e. _V -> ( ordTop ` <_ ) = ( TopSet ` G ) )
242 65 241 ax-mp 
 |-  ( ordTop ` <_ ) = ( TopSet ` G )
243 8 242 topnval 
 |-  ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) = ( TopOpen ` G )
244 eqid 
 |-  ( ~P A i^i Fin ) = ( ~P A i^i Fin )
245 27 a1i 
 |-  ( ph -> G e. CMnd )
246 xrstps 
 |-  RR*s e. TopSp
247 resstps 
 |-  ( ( RR*s e. TopSp /\ ( 0 [,] +oo ) e. _V ) -> ( RR*s |`s ( 0 [,] +oo ) ) e. TopSp )
248 246 65 247 mp2an 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. TopSp
249 1 248 eqeltri 
 |-  G e. TopSp
250 249 a1i 
 |-  ( ph -> G e. TopSp )
251 8 243 244 245 250 2 3 eltsms 
 |-  ( ph -> ( S e. ( G tsums F ) <-> ( S e. ( 0 [,] +oo ) /\ A. u e. ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) ( S e. u -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. u ) ) ) ) )
252 63 239 251 mpbir2and 
 |-  ( ph -> S e. ( G tsums F ) )
253 letsr 
 |-  <_ e. TosetRel
254 ordthaus 
 |-  ( <_ e. TosetRel -> ( ordTop ` <_ ) e. Haus )
255 253 254 mp1i 
 |-  ( ph -> ( ordTop ` <_ ) e. Haus )
256 resthaus 
 |-  ( ( ( ordTop ` <_ ) e. Haus /\ ( 0 [,] +oo ) e. _V ) -> ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) e. Haus )
257 255 65 256 sylancl 
 |-  ( ph -> ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) e. Haus )
258 8 245 250 2 3 243 257 haustsms2 
 |-  ( ph -> ( S e. ( G tsums F ) -> ( G tsums F ) = { S } ) )
259 252 258 mpd 
 |-  ( ph -> ( G tsums F ) = { S } )