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	|- G = ( RR*s |`s ( 0 [,] +oo ) )
	xrge0tsmseq.a	|- ( ph -> A e. V )
	xrge0tsmseq.f	|- ( ph -> F : A --> ( 0 [,] +oo ) )
Assertion	xrge0tsmsbi	|- ( ph -> ( C e. ( G tsums F ) <-> C = U. ( G tsums F ) ) )

Proof

Step	Hyp	Ref	Expression
1		xrge0tsmseq.g	|- G = ( RR*s |`s ( 0 [,] +oo ) )
2		xrge0tsmseq.a	|- ( ph -> A e. V )
3		xrge0tsmseq.f	|- ( ph -> F : A --> ( 0 [,] +oo ) )
4	1	xrge0tsms2	|- ( ( A e. V /\ F : A --> ( 0 [,] +oo ) ) -> ( G tsums F ) ~~ 1o )
5	2 3 4	syl2anc	|- ( ph -> ( G tsums F ) ~~ 1o )
6		en1b	|- ( ( G tsums F ) ~~ 1o <-> ( G tsums F ) = { U. ( G tsums F ) } )
7	5 6	sylib	|- ( ph -> ( G tsums F ) = { U. ( G tsums F ) } )
8	7	eleq2d	|- ( ph -> ( C e. ( G tsums F ) <-> C e. { U. ( G tsums F ) } ) )
9		ovex	|- ( G tsums F ) e. _V
10	9	uniex	|- U. ( G tsums F ) e. _V
11		eleq1	|- ( C = U. ( G tsums F ) -> ( C e. _V <-> U. ( G tsums F ) e. _V ) )
12	10 11	mpbiri	|- ( C = U. ( G tsums F ) -> C e. _V )
13		elsng	|- ( C e. _V -> ( C e. { U. ( G tsums F ) } <-> C = U. ( G tsums F ) ) )
14	12 13	syl	|- ( C = U. ( G tsums F ) -> ( C e. { U. ( G tsums F ) } <-> C = U. ( G tsums F ) ) )
15	14	ibir	|- ( C = U. ( G tsums F ) -> C e. { U. ( G tsums F ) } )
16		elsni	|- ( C e. { U. ( G tsums F ) } -> C = U. ( G tsums F ) )
17	15 16	impbii	|- ( C = U. ( G tsums F ) <-> C e. { U. ( G tsums F ) } )
18	8 17	bitr4di	|- ( ph -> ( C e. ( G tsums F ) <-> C = U. ( G tsums F ) ) )