Theorem xrge0tsmsbi

Description: Any limit of a finite or infinite sum in the nonnegative extended reals is the union of the sets limits, since this set is a singleton. (Contributed by Thierry Arnoux, 23-Jun-2017)

	Ref	Expression
Hypotheses	xrge0tsmseq.g	⊢ 𝐺 = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
	xrge0tsmseq.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	xrge0tsmseq.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ( 0 [,] +∞ ) )
Assertion	xrge0tsmsbi	⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐺 tsums 𝐹 ) ↔ 𝐶 = ∪ ( 𝐺 tsums 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		xrge0tsmseq.g	⊢ 𝐺 = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
2		xrge0tsmseq.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		xrge0tsmseq.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ( 0 [,] +∞ ) )
4	1	xrge0tsms2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ( 0 [,] +∞ ) ) → ( 𝐺 tsums 𝐹 ) ≈ 1o )
5	2 3 4	syl2anc	⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) ≈ 1o )
6		en1b	⊢ ( ( 𝐺 tsums 𝐹 ) ≈ 1o ↔ ( 𝐺 tsums 𝐹 ) = { ∪ ( 𝐺 tsums 𝐹 ) } )
7	5 6	sylib	⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) = { ∪ ( 𝐺 tsums 𝐹 ) } )
8	7	eleq2d	⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐺 tsums 𝐹 ) ↔ 𝐶 ∈ { ∪ ( 𝐺 tsums 𝐹 ) } ) )
9		ovex	⊢ ( 𝐺 tsums 𝐹 ) ∈ V
10	9	uniex	⊢ ∪ ( 𝐺 tsums 𝐹 ) ∈ V
11		eleq1	⊢ ( 𝐶 = ∪ ( 𝐺 tsums 𝐹 ) → ( 𝐶 ∈ V ↔ ∪ ( 𝐺 tsums 𝐹 ) ∈ V ) )
12	10 11	mpbiri	⊢ ( 𝐶 = ∪ ( 𝐺 tsums 𝐹 ) → 𝐶 ∈ V )
13		elsng	⊢ ( 𝐶 ∈ V → ( 𝐶 ∈ { ∪ ( 𝐺 tsums 𝐹 ) } ↔ 𝐶 = ∪ ( 𝐺 tsums 𝐹 ) ) )
14	12 13	syl	⊢ ( 𝐶 = ∪ ( 𝐺 tsums 𝐹 ) → ( 𝐶 ∈ { ∪ ( 𝐺 tsums 𝐹 ) } ↔ 𝐶 = ∪ ( 𝐺 tsums 𝐹 ) ) )
15	14	ibir	⊢ ( 𝐶 = ∪ ( 𝐺 tsums 𝐹 ) → 𝐶 ∈ { ∪ ( 𝐺 tsums 𝐹 ) } )
16		elsni	⊢ ( 𝐶 ∈ { ∪ ( 𝐺 tsums 𝐹 ) } → 𝐶 = ∪ ( 𝐺 tsums 𝐹 ) )
17	15 16	impbii	⊢ ( 𝐶 = ∪ ( 𝐺 tsums 𝐹 ) ↔ 𝐶 ∈ { ∪ ( 𝐺 tsums 𝐹 ) } )
18	8 17	bitr4di	⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐺 tsums 𝐹 ) ↔ 𝐶 = ∪ ( 𝐺 tsums 𝐹 ) ) )