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=ℝ𝑠*↾𝑠0+∞
xrge0tsmseq.a ⊢φ→A∈V
xrge0tsmseq.f ⊢φ→F:A⟶0+∞
Assertion xrge0tsmsbi ⊢φ→C∈GtsumsF↔C=⋃GtsumsF

Proof

Step Hyp Ref Expression
1 xrge0tsmseq.g ⊢G=ℝ𝑠*↾𝑠0+∞
2 xrge0tsmseq.a ⊢φ→A∈V
3 xrge0tsmseq.f ⊢φ→F:A⟶0+∞
4 1 xrge0tsms2 ⊢A∈V∧F:A⟶0+∞→GtsumsF≈1𝑜
5 2 3 4 syl2anc ⊢φ→GtsumsF≈1𝑜
6 en1b ⊢GtsumsF≈1𝑜↔GtsumsF=⋃GtsumsF
7 5 6 sylib ⊢φ→GtsumsF=⋃GtsumsF
8 7 eleq2d ⊢φ→C∈GtsumsF↔C∈⋃GtsumsF
9 ovex ⊢GtsumsF∈V
10 9 uniex ⊢⋃GtsumsF∈V
11 eleq1 ⊢C=⋃GtsumsF→C∈V↔⋃GtsumsF∈V
12 10 11 mpbiri ⊢C=⋃GtsumsF→C∈V
13 elsng ⊢C∈V→C∈⋃GtsumsF↔C=⋃GtsumsF
14 12 13 syl ⊢C=⋃GtsumsF→C∈⋃GtsumsF↔C=⋃GtsumsF
15 14 ibir ⊢C=⋃GtsumsF→C∈⋃GtsumsF
16 elsni ⊢C∈⋃GtsumsF→C=⋃GtsumsF
17 15 16 impbii ⊢C=⋃GtsumsF↔C∈⋃GtsumsF
18 8 17 bitr4di ⊢φ→C∈GtsumsF↔C=⋃GtsumsF