This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xrge0tsmsd

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) (Revised by Thierry Arnoux, 30-Jan-2017)

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

Proof

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