Definition df-sumge0

Description: Define the arbitrary sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020) $.

	Ref	Expression
Assertion	df-sumge0	⊢ Σ^ = ( 𝑥 ∈ V ↦ if ( +∞ ∈ ran 𝑥 , +∞ , sup ( ran ( 𝑦 ∈ ( 𝒫 dom 𝑥 ∩ Fin ) ↦ Σ 𝑤 ∈ 𝑦 ( 𝑥 ‘ 𝑤 ) ) , ℝ* , < ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csumge0	⊢ Σ^
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		cpnf	⊢ +∞
4	1	cv	⊢ 𝑥
5	4	crn	⊢ ran 𝑥
6	3 5	wcel	⊢ +∞ ∈ ran 𝑥
7		vy	⊢ 𝑦
8	4	cdm	⊢ dom 𝑥
9	8	cpw	⊢ 𝒫 dom 𝑥
10		cfn	⊢ Fin
11	9 10	cin	⊢ ( 𝒫 dom 𝑥 ∩ Fin )
12		vw	⊢ 𝑤
13	7	cv	⊢ 𝑦
14	12	cv	⊢ 𝑤
15	14 4	cfv	⊢ ( 𝑥 ‘ 𝑤 )
16	13 15 12	csu	⊢ Σ 𝑤 ∈ 𝑦 ( 𝑥 ‘ 𝑤 )
17	7 11 16	cmpt	⊢ ( 𝑦 ∈ ( 𝒫 dom 𝑥 ∩ Fin ) ↦ Σ 𝑤 ∈ 𝑦 ( 𝑥 ‘ 𝑤 ) )
18	17	crn	⊢ ran ( 𝑦 ∈ ( 𝒫 dom 𝑥 ∩ Fin ) ↦ Σ 𝑤 ∈ 𝑦 ( 𝑥 ‘ 𝑤 ) )
19		cxr	⊢ ℝ*
20		clt	⊢ <
21	18 19 20	csup	⊢ sup ( ran ( 𝑦 ∈ ( 𝒫 dom 𝑥 ∩ Fin ) ↦ Σ 𝑤 ∈ 𝑦 ( 𝑥 ‘ 𝑤 ) ) , ℝ* , < )
22	6 3 21	cif	⊢ if ( +∞ ∈ ran 𝑥 , +∞ , sup ( ran ( 𝑦 ∈ ( 𝒫 dom 𝑥 ∩ Fin ) ↦ Σ 𝑤 ∈ 𝑦 ( 𝑥 ‘ 𝑤 ) ) , ℝ* , < ) )
23	1 2 22	cmpt	⊢ ( 𝑥 ∈ V ↦ if ( +∞ ∈ ran 𝑥 , +∞ , sup ( ran ( 𝑦 ∈ ( 𝒫 dom 𝑥 ∩ Fin ) ↦ Σ 𝑤 ∈ 𝑦 ( 𝑥 ‘ 𝑤 ) ) , ℝ* , < ) ) )
24	0 23	wceq	⊢ Σ^ = ( 𝑥 ∈ V ↦ if ( +∞ ∈ ran 𝑥 , +∞ , sup ( ran ( 𝑦 ∈ ( 𝒫 dom 𝑥 ∩ Fin ) ↦ Σ 𝑤 ∈ 𝑦 ( 𝑥 ‘ 𝑤 ) ) , ℝ* , < ) ) )