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

Proof

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