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 sselid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑍 ∩ 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 sselid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
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 bilani ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) ) → ∃ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 )
49 2 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) → 𝑀 ∈ ℤ )
50 17 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) → 𝑥 ⊆ 𝑍 )
51 14 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) → 𝑥 ∈ Fin )
52 49 3 50 51 uzfissfz ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) → ∃ 𝑛 ∈ 𝑍 𝑥 ⊆ ( 𝑀 ... 𝑛 ) )
53 nfv ⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 )
54 nfmpt1 ⊢ Ⅎ 𝑛 ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 )
55 54 nfrn ⊢ Ⅎ 𝑛 ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 )
56 nfv ⊢ Ⅎ 𝑛 𝑦 ≤ 𝑤
57 55 56 nfrexw ⊢ Ⅎ 𝑛 ∃ 𝑤 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) 𝑦 ≤ 𝑤
58 id ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ 𝑍 )
59 sumex ⊢ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ∈ V
60 59 a1i ⊢ ( 𝑛 ∈ 𝑍 → Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ∈ V )
61 30 elrnmpt1 ⊢ ( ( 𝑛 ∈ 𝑍 ∧ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ∈ V ) → Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) )
62 58 60 61 syl2anc ⊢ ( 𝑛 ∈ 𝑍 → Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) )
63 62 3ad2ant2 ⊢ ( ( ( 𝜑 ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ⊆ ( 𝑀 ... 𝑛 ) ) → Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) )
64 simplr ⊢ ( ( ( 𝜑 ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑥 ⊆ ( 𝑀 ... 𝑛 ) ) → 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 )
65 nfcv ⊢ Ⅎ 𝑘 𝑦
66 nfcv ⊢ Ⅎ 𝑘 𝑥
67 66 nfsum1 ⊢ Ⅎ 𝑘 Σ 𝑘 ∈ 𝑥 𝐵
68 65 67 nfeq ⊢ Ⅎ 𝑘 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵
69 1 68 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 )
70 nfv ⊢ Ⅎ 𝑘 𝑥 ⊆ ( 𝑀 ... 𝑛 )
71 69 70 nfan ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑥 ⊆ ( 𝑀 ... 𝑛 ) )
72 fzfid ⊢ ( ( ( 𝜑 ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑥 ⊆ ( 𝑀 ... 𝑛 ) ) → ( 𝑀 ... 𝑛 ) ∈ Fin )
73 38 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑥 ⊆ ( 𝑀 ... 𝑛 ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → 𝐵 ∈ ℝ )
74 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑥 ⊆ ( 𝑀 ... 𝑛 ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → 𝜑 )
75 35 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑥 ⊆ ( 𝑀 ... 𝑛 ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → 𝑘 ∈ 𝑍 )
76 0xr ⊢ 0 ∈ ℝ*
77 76 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 0 ∈ ℝ* )
78 pnfxr ⊢ +∞ ∈ ℝ*
79 78 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → +∞ ∈ ℝ* )
80 icogelb ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → 0 ≤ 𝐵 )
81 77 79 4 80 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 0 ≤ 𝐵 )
82 74 75 81 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑥 ⊆ ( 𝑀 ... 𝑛 ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → 0 ≤ 𝐵 )
83 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑥 ⊆ ( 𝑀 ... 𝑛 ) ) → 𝑥 ⊆ ( 𝑀 ... 𝑛 ) )
84 71 72 73 82 83 fsumlessf ⊢ ( ( ( 𝜑 ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑥 ⊆ ( 𝑀 ... 𝑛 ) ) → Σ 𝑘 ∈ 𝑥 𝐵 ≤ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 )
85 64 84 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑥 ⊆ ( 𝑀 ... 𝑛 ) ) → 𝑦 ≤ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 )
86 85 3adant2 ⊢ ( ( ( 𝜑 ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ⊆ ( 𝑀 ... 𝑛 ) ) → 𝑦 ≤ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 )
87 breq2 ⊢ ( 𝑤 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 → ( 𝑦 ≤ 𝑤 ↔ 𝑦 ≤ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) )
88 87 rspcev ⊢ ( ( Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) ∧ 𝑦 ≤ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) → ∃ 𝑤 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) 𝑦 ≤ 𝑤 )
89 63 86 88 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ⊆ ( 𝑀 ... 𝑛 ) ) → ∃ 𝑤 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) 𝑦 ≤ 𝑤 )
90 89 3exp ⊢ ( ( 𝜑 ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) → ( 𝑛 ∈ 𝑍 → ( 𝑥 ⊆ ( 𝑀 ... 𝑛 ) → ∃ 𝑤 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) 𝑦 ≤ 𝑤 ) ) )
91 90 3adant2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) → ( 𝑛 ∈ 𝑍 → ( 𝑥 ⊆ ( 𝑀 ... 𝑛 ) → ∃ 𝑤 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) 𝑦 ≤ 𝑤 ) ) )
92 53 57 91 rexlimd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) → ( ∃ 𝑛 ∈ 𝑍 𝑥 ⊆ ( 𝑀 ... 𝑛 ) → ∃ 𝑤 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) 𝑦 ≤ 𝑤 ) )
93 52 92 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) → ∃ 𝑤 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) 𝑦 ≤ 𝑤 )
94 93 3exp ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) → ( 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 → ∃ 𝑤 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) 𝑦 ≤ 𝑤 ) ) )
95 94 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 → ∃ 𝑤 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) 𝑦 ≤ 𝑤 ) )
96 95 imp ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 ) → ∃ 𝑤 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) 𝑦 ≤ 𝑤 )
97 48 96 syldan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) ) → ∃ 𝑤 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) 𝑦 ≤ 𝑤 )
98 26 42 97 suplesup2 ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) , ℝ* , < ) ≤ sup ( ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) , ℝ* , < ) )
99 30 elrnmpt ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) ↔ ∃ 𝑛 ∈ 𝑍 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) )
100 45 99 ax-mp ⊢ ( 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) ↔ ∃ 𝑛 ∈ 𝑍 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 )
101 100 bilani ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) ) → ∃ 𝑛 ∈ 𝑍 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 )
102 35 ssriv ⊢ ( 𝑀 ... 𝑛 ) ⊆ 𝑍
103 ovex ⊢ ( 𝑀 ... 𝑛 ) ∈ V
104 103 elpw ⊢ ( ( 𝑀 ... 𝑛 ) ∈ 𝒫 𝑍 ↔ ( 𝑀 ... 𝑛 ) ⊆ 𝑍 )
105 102 104 mpbir ⊢ ( 𝑀 ... 𝑛 ) ∈ 𝒫 𝑍
106 fzfi ⊢ ( 𝑀 ... 𝑛 ) ∈ Fin
107 105 106 elini ⊢ ( 𝑀 ... 𝑛 ) ∈ ( 𝒫 𝑍 ∩ Fin )
108 107 a1i ⊢ ( 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 → ( 𝑀 ... 𝑛 ) ∈ ( 𝒫 𝑍 ∩ Fin ) )
109 id ⊢ ( 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 → 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 )
110 sumeq1 ⊢ ( 𝑥 = ( 𝑀 ... 𝑛 ) → Σ 𝑘 ∈ 𝑥 𝐵 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 )
111 110 rspceeqv ⊢ ( ( ( 𝑀 ... 𝑛 ) ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) → ∃ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 )
112 108 109 111 syl2anc ⊢ ( 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 → ∃ 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) 𝑦 = Σ 𝑘 ∈ 𝑥 𝐵 )
113 45 a1i ⊢ ( 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 → 𝑦 ∈ V )
114 10 112 113 elrnmptd ⊢ ( 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 → 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) )
115 114 2a1i ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 → ( 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 → 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) ) ) )
116 115 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑛 ∈ 𝑍 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 → 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) ) )
117 116 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) ) → ( ∃ 𝑛 ∈ 𝑍 𝑦 = Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 → 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) ) )
118 101 117 mpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) ) → 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) )
119 118 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) )
120 dfss3 ⊢ ( ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) ⊆ ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) ↔ ∀ 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) )
121 119 120 sylibr ⊢ ( 𝜑 → ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) ⊆ ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) )
122 supxrss ⊢ ( ( ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) ⊆ ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) ∧ ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) ⊆ ℝ* ) → sup ( ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) , ℝ* , < ) ≤ sup ( ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) , ℝ* , < ) )
123 121 26 122 syl2anc ⊢ ( 𝜑 → sup ( ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) , ℝ* , < ) ≤ sup ( ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) , ℝ* , < ) )
124 28 44 98 123 xrletrid ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑍 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐵 ) , ℝ* , < ) = sup ( ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) , ℝ* , < ) )
125 8 124 eqtrd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ) = sup ( ran ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐵 ) , ℝ* , < ) )