Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-sumge0 Structured version   Visualization version   GIF version

Definition df-sumge0 41059
Description: Define the arbitrary sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) $.
Assertion
Ref Expression
df-sumge0 Σ^ = (𝑥 ∈ V ↦ if(+∞ ∈ ran 𝑥, +∞, sup(ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤𝑦 (𝑥𝑤)), ℝ*, < )))
Distinct variable group:   𝑥,𝑤,𝑦

Detailed syntax breakdown of Definition df-sumge0
StepHypRef Expression
1 csumge0 41058 . 2 class Σ^
2 vx . . 3 setvar 𝑥
3 cvv 3391 . . 3 class V
4 cpnf 10356 . . . . 5 class +∞
52cv 1636 . . . . . 6 class 𝑥
65crn 5312 . . . . 5 class ran 𝑥
74, 6wcel 2156 . . . 4 wff +∞ ∈ ran 𝑥
8 vy . . . . . . 7 setvar 𝑦
95cdm 5311 . . . . . . . . 9 class dom 𝑥
109cpw 4351 . . . . . . . 8 class 𝒫 dom 𝑥
11 cfn 8192 . . . . . . . 8 class Fin
1210, 11cin 3768 . . . . . . 7 class (𝒫 dom 𝑥 ∩ Fin)
138cv 1636 . . . . . . . 8 class 𝑦
14 vw . . . . . . . . . 10 setvar 𝑤
1514cv 1636 . . . . . . . . 9 class 𝑤
1615, 5cfv 6101 . . . . . . . 8 class (𝑥𝑤)
1713, 16, 14csu 14639 . . . . . . 7 class Σ𝑤𝑦 (𝑥𝑤)
188, 12, 17cmpt 4923 . . . . . 6 class (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤𝑦 (𝑥𝑤))
1918crn 5312 . . . . 5 class ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤𝑦 (𝑥𝑤))
20 cxr 10358 . . . . 5 class *
21 clt 10359 . . . . 5 class <
2219, 20, 21csup 8585 . . . 4 class sup(ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤𝑦 (𝑥𝑤)), ℝ*, < )
237, 4, 22cif 4279 . . 3 class if(+∞ ∈ ran 𝑥, +∞, sup(ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤𝑦 (𝑥𝑤)), ℝ*, < ))
242, 3, 23cmpt 4923 . 2 class (𝑥 ∈ V ↦ if(+∞ ∈ ran 𝑥, +∞, sup(ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤𝑦 (𝑥𝑤)), ℝ*, < )))
251, 24wceq 1637 1 wff Σ^ = (𝑥 ∈ V ↦ if(+∞ ∈ ran 𝑥, +∞, sup(ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤𝑦 (𝑥𝑤)), ℝ*, < )))
Colors of variables: wff setvar class
This definition is referenced by:  sge0val  41062
  Copyright terms: Public domain W3C validator