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 𝐺 = ( ℝ*𝑠s ( 0 [,] +∞ ) )
xrge0tsms.a ( 𝜑𝐴𝑉 )
xrge0tsms.f ( 𝜑𝐹 : 𝐴 ⟶ ( 0 [,] +∞ ) )
xrge0tsms.s 𝑆 = sup ( ran ( 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹𝑠 ) ) ) , ℝ* , < )
Assertion xrge0tsms ( 𝜑 → ( 𝐺 tsums 𝐹 ) = { 𝑆 } )

Proof

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