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 ⊢ 𝐺 = ( ℝ*𝑠 ↾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 𝐹 ) ) )