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 ∈ G tsums F ↔ C = ⋃ G tsums F

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 +∞ → G tsums F ≈ 1 𝑜
5 2 3 4 syl2anc ⊢ φ → G tsums F ≈ 1 𝑜
6 en1b ⊢ G tsums F ≈ 1 𝑜 ↔ G tsums F = ⋃ G tsums F
7 5 6 sylib ⊢ φ → G tsums F = ⋃ G tsums F
8 7 eleq2d ⊢ φ → C ∈ G tsums F ↔ C ∈ ⋃ G tsums F
9 ovex ⊢ G tsums F ∈ V
10 9 uniex ⊢ ⋃ G tsums F ∈ V
11 eleq1 ⊢ C = ⋃ G tsums F → C ∈ V ↔ ⋃ G tsums F ∈ V
12 10 11 mpbiri ⊢ C = ⋃ G tsums F → C ∈ V
13 elsng ⊢ C ∈ V → C ∈ ⋃ G tsums F ↔ C = ⋃ G tsums F
14 12 13 syl ⊢ C = ⋃ G tsums F → C ∈ ⋃ G tsums F ↔ C = ⋃ G tsums F
15 14 ibir ⊢ C = ⋃ G tsums F → C ∈ ⋃ G tsums F
16 elsni ⊢ C ∈ ⋃ G tsums F → C = ⋃ G tsums F
17 15 16 impbii ⊢ C = ⋃ G tsums F ↔ C ∈ ⋃ G tsums F
18 8 17 bitr4di ⊢ φ → C ∈ G tsums F ↔ C = ⋃ G tsums F