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 0fi ⊢ ∅ ∈ 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 biimtrid ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 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 biimtrid ⊢ ( 𝜑 → ( 𝑢 ∈ ( ( 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 𝐹 ) = { 𝑆 } )