Metamath Proof Explorer

Theorem sge0reuz

Description: Value of the generalized sum of nonnegative reals, when the domain is a set of upper integers. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses sge0reuz.k ⊢ Ⅎ 𝑘 𝜑
sge0reuz.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
sge0reuz.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
sge0reuz.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
Assertion sge0reuz ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ) = sup ( ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 sge0reuz.k ⊢ Ⅎ 𝑘 𝜑
2 sge0reuz.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 sge0reuz.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4 sge0reuz.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
5 3 a1i ⊢ ( 𝜑 → 𝑍 = ( ℤ≥ ‘ 𝑀 ) )
6 fvex ⊢ ( ℤ≥ ‘ 𝑀 ) ∈ V
7 5 6 eqeltrdi ⊢ ( 𝜑 → 𝑍 ∈ V )
8 1 7 4 sge0revalmpt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) , ℝ* , < ) )
9 nfv ⊢ Ⅎ 𝑥 𝜑
10 eqid ⊢ ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) = ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 )
11 nfv ⊢ Ⅎ 𝑘 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin )
12 1 11 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) )
13 elinel2 ⊢ ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) → 𝑥 ∈ Fin )
14 13 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → 𝑥 ∈ Fin )
15 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
16 simpll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝜑 )
17 elpwinss ⊢ ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) → 𝑥 ⊆ 𝑍 )
18 17 adantr ⊢ ( ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝑘 ∈ 𝑥 ) → 𝑥 ⊆ 𝑍 )
19 simpr ⊢ ( ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝑘 ∈ 𝑥 ) → 𝑘 ∈ 𝑥 )
20 18 19 sseldd ⊢ ( ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝑘 ∈ 𝑥 ) → 𝑘 ∈ 𝑍 )
21 20 adantll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝑘 ∈ 𝑍 )
22 16 21 4 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
23 15 22 sseldi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝐵 ∈ ℝ )
24 12 14 23 fsumreclf ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑥 𝐵 ∈ ℝ )
25 24 rexrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑥 𝐵 ∈ ℝ* )
26 9 10 25 rnmptssd ⊢ ( 𝜑 → ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) ⊆ ℝ* )
27 supxrcl ⊢ ( ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) ⊆ ℝ* → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) , ℝ* , < ) ∈ ℝ* )
28 26 27 syl ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) , ℝ* , < ) ∈ ℝ* )
29 nfv ⊢ Ⅎ 𝑛 𝜑
30 eqid ⊢ ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) = ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 )
31 nfv ⊢ Ⅎ 𝑘 𝑛 ∈ 𝑍
32 1 31 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑛 ∈ 𝑍 )
33 fzfid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑀 ... 𝑛 ) ∈ Fin )
34 elfzuz ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑛 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
35 34 3 eleqtrrdi ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑛 ) → 𝑘 ∈ 𝑍 )
36 35 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → 𝑘 ∈ 𝑍 )
37 15 4 sseldi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
38 36 37 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → 𝐵 ∈ ℝ )
39 38 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → 𝐵 ∈ ℝ )
40 32 33 39 fsumreclf ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ∈ ℝ )
41 40 rexrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ∈ ℝ* )
42 29 30 41 rnmptssd ⊢ ( 𝜑 → ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) ⊆ ℝ* )
43 supxrcl ⊢ ( ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) ⊆ ℝ* → sup ( ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) , ℝ* , < ) ∈ ℝ* )
44 42 43 syl ⊢ ( 𝜑 → sup ( ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) , ℝ* , < ) ∈ ℝ* )
45 vex ⊢ 𝑦 ∈ V
46 10 elrnmpt ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) )
47 45 46 ax-mp ⊢ ( 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 )
48 47 biimpi ⊢ ( 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) → ∃ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 )
49 48 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) ) → ∃ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 )
50 2 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) → 𝑀 ∈ ℤ )
51 17 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) → 𝑥 ⊆ 𝑍 )
52 14 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) → 𝑥 ∈ Fin )
53 50 3 51 52 uzfissfz ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) → ∃ 𝑛 ∈ 𝑍 𝑥 ⊆ ( 𝑀 ... 𝑛 ) )
54 nfv ⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 )
55 nfmpt1 ⊢ Ⅎ 𝑛 ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 )
56 55 nfrn ⊢ Ⅎ 𝑛 ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 )
57 nfv ⊢ Ⅎ 𝑛 𝑦 ≤ 𝑤
58 56 57 nfrex ⊢ Ⅎ 𝑛 ∃ 𝑤 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) 𝑦 ≤ 𝑤
59 id ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ 𝑍 )
60 sumex ⊢ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ∈ V
61 60 a1i ⊢ ( 𝑛 ∈ 𝑍 → Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ∈ V )
62 30 elrnmpt1 ⊢ ( ( 𝑛 ∈ 𝑍 ∧ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ∈ V ) → Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) )
63 59 61 62 syl2anc ⊢ ( 𝑛 ∈ 𝑍 → Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) )
64 63 3ad2ant2 ⊢ ( ( ( 𝜑 ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ⊆ ( 𝑀 ... 𝑛 ) ) → Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) )
65 simplr ⊢ ( ( ( 𝜑 ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑥 ⊆ ( 𝑀 ... 𝑛 ) ) → 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 )
66 nfcv ⊢ Ⅎ 𝑘 𝑦
67 nfcv ⊢ Ⅎ 𝑘 𝑥
68 67 nfsum1 ⊢ Ⅎ 𝑘 Σ 𝑘 ∈ 𝑥 𝐵
69 66 68 nfeq ⊢ Ⅎ 𝑘 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵
70 1 69 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 )
71 nfv ⊢ Ⅎ 𝑘 𝑥 ⊆ ( 𝑀 ... 𝑛 )
72 70 71 nfan ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑥 ⊆ ( 𝑀 ... 𝑛 ) )
73 fzfid ⊢ ( ( ( 𝜑 ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑥 ⊆ ( 𝑀 ... 𝑛 ) ) → ( 𝑀 ... 𝑛 ) ∈ Fin )
74 38 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑥 ⊆ ( 𝑀 ... 𝑛 ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → 𝐵 ∈ ℝ )
75 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑥 ⊆ ( 𝑀 ... 𝑛 ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → 𝜑 )
76 35 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑥 ⊆ ( 𝑀 ... 𝑛 ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → 𝑘 ∈ 𝑍 )
77 0xr ⊢ 0 ∈ ℝ*
78 77 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 0 ∈ ℝ* )
79 pnfxr ⊢ +∞ ∈ ℝ*
80 79 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → +∞ ∈ ℝ* )
81 icogelb ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → 0 ≤ 𝐵 )
82 78 80 4 81 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 0 ≤ 𝐵 )
83 75 76 82 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑥 ⊆ ( 𝑀 ... 𝑛 ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → 0 ≤ 𝐵 )
84 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑥 ⊆ ( 𝑀 ... 𝑛 ) ) → 𝑥 ⊆ ( 𝑀 ... 𝑛 ) )
85 72 73 74 83 84 fsumlessf ⊢ ( ( ( 𝜑 ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑥 ⊆ ( 𝑀 ... 𝑛 ) ) → Σ 𝑘 ∈ 𝑥 𝐵 ≤ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 )
86 65 85 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑥 ⊆ ( 𝑀 ... 𝑛 ) ) → 𝑦 ≤ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 )
87 86 3adant2 ⊢ ( ( ( 𝜑 ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ⊆ ( 𝑀 ... 𝑛 ) ) → 𝑦 ≤ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 )
88 breq2 ⊢ ( 𝑤 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 → ( 𝑦 ≤ 𝑤 ↔ 𝑦 ≤ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) )
89 88 rspcev ⊢ ( ( Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) ∧ 𝑦 ≤ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) → ∃ 𝑤 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) 𝑦 ≤ 𝑤 )
90 64 87 89 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ⊆ ( 𝑀 ... 𝑛 ) ) → ∃ 𝑤 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) 𝑦 ≤ 𝑤 )
91 90 3exp ⊢ ( ( 𝜑 ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) → ( 𝑛 ∈ 𝑍 → ( 𝑥 ⊆ ( 𝑀 ... 𝑛 ) → ∃ 𝑤 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) 𝑦 ≤ 𝑤 ) ) )
92 91 3adant2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) → ( 𝑛 ∈ 𝑍 → ( 𝑥 ⊆ ( 𝑀 ... 𝑛 ) → ∃ 𝑤 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) 𝑦 ≤ 𝑤 ) ) )
93 54 58 92 rexlimd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) → ( ∃ 𝑛 ∈ 𝑍 𝑥 ⊆ ( 𝑀 ... 𝑛 ) → ∃ 𝑤 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) 𝑦 ≤ 𝑤 ) )
94 53 93 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) → ∃ 𝑤 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) 𝑦 ≤ 𝑤 )
95 94 3exp ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) → ( 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 → ∃ 𝑤 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) 𝑦 ≤ 𝑤 ) ) )
96 95 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 → ∃ 𝑤 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) 𝑦 ≤ 𝑤 ) )
97 96 imp ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) → ∃ 𝑤 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) 𝑦 ≤ 𝑤 )
98 49 97 syldan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) ) → ∃ 𝑤 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) 𝑦 ≤ 𝑤 )
99 26 42 98 suplesup2 ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) , ℝ* , < ) ≤ sup ( ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) , ℝ* , < ) )
100 30 elrnmpt ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) ↔ ∃ 𝑛 ∈ 𝑍 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) )
101 45 100 ax-mp ⊢ ( 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) ↔ ∃ 𝑛 ∈ 𝑍 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 )
102 101 biimpi ⊢ ( 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) → ∃ 𝑛 ∈ 𝑍 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 )
103 102 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) ) → ∃ 𝑛 ∈ 𝑍 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 )
104 35 ssriv ⊢ ( 𝑀 ... 𝑛 ) ⊆ 𝑍
105 ovex ⊢ ( 𝑀 ... 𝑛 ) ∈ V
106 105 elpw ⊢ ( ( 𝑀 ... 𝑛 ) ∈ 𝒫 𝑍 ↔ ( 𝑀 ... 𝑛 ) ⊆ 𝑍 )
107 104 106 mpbir ⊢ ( 𝑀 ... 𝑛 ) ∈ 𝒫 𝑍
108 fzfi ⊢ ( 𝑀 ... 𝑛 ) ∈ Fin
109 107 108 elini ⊢ ( 𝑀 ... 𝑛 ) ∈ ( 𝒫 𝑍 ∩ Fin )
110 109 a1i ⊢ ( 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 → ( 𝑀 ... 𝑛 ) ∈ ( 𝒫 𝑍 ∩ Fin ) )
111 id ⊢ ( 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 → 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 )
112 sumeq1 ⊢ ( 𝑥 = ( 𝑀 ... 𝑛 ) → Σ 𝑘 ∈ 𝑥 𝐵 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 )
113 112 rspceeqv ⊢ ( ( ( 𝑀 ... 𝑛 ) ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) → ∃ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 )
114 110 111 113 syl2anc ⊢ ( 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 → ∃ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 )
115 45 a1i ⊢ ( 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 → 𝑦 ∈ V )
116 10 114 115 elrnmptd ⊢ ( 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 → 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) )
117 116 2a1i ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 → ( 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 → 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) ) ) )
118 117 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑛 ∈ 𝑍 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 → 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) ) )
119 118 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) ) → ( ∃ 𝑛 ∈ 𝑍 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 → 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) ) )
120 103 119 mpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) ) → 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) )
121 120 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) )
122 dfss3 ⊢ ( ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) ⊆ ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) ↔ ∀ 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) )
123 121 122 sylibr ⊢ ( 𝜑 → ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) ⊆ ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) )
124 supxrss ⊢ ( ( ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) ⊆ ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) ⊆ ℝ* ) → sup ( ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) , ℝ* , < ) ≤ sup ( ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) , ℝ* , < ) )
125 123 26 124 syl2anc ⊢ ( 𝜑 → sup ( ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) , ℝ* , < ) ≤ sup ( ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) , ℝ* , < ) )
126 28 44 99 125 xrletrid ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) , ℝ* , < ) = sup ( ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) , ℝ* , < ) )
127 8 126 eqtrd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ) = sup ( ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) , ℝ* , < ) )