This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )