Theorem esumid

Description: Identify the extended sum as any limit points of the infinite sum. (Contributed by Thierry Arnoux, 9-May-2017)

	Ref	Expression
Hypotheses	esumid.p	$$⊢Ⅎk\phi$$
	esumid.0	$$⊢\underset{\_}{Ⅎ}kA$$
	esumid.1	$$⊢\phi \to A\in V$$
	esumid.2	$$⊢\left(\phi \wedge k\in A\right)\to B\in \left[0,\mathrm{+\infty }\right]$$
	esumid.3	$$⊢\phi \to C\in \left(\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left(k\in A⟼B\right)\right)$$
Assertion	esumid	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}B=C$$

Proof

Step	Hyp	Ref	Expression
1		esumid.p	$$⊢Ⅎk\phi$$
2		esumid.0	$$⊢\underset{\_}{Ⅎ}kA$$
3		esumid.1	$$⊢\phi \to A\in V$$
4		esumid.2	$$⊢\left(\phi \wedge k\in A\right)\to B\in \left[0,\mathrm{+\infty }\right]$$
5		esumid.3	$$⊢\phi \to C\in \left(\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left(k\in A⟼B\right)\right)$$
6		df-esum	$$⊢\underset{k\in A}{{\sum }^{*}}B=\bigcup \left(\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left(k\in A⟼B\right)\right)$$
7		eqid	$$⊢{ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]={ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}k\left[0,\mathrm{+\infty }\right]$$
9		eqid	$$⊢\left(k\in A⟼B\right)=\left(k\in A⟼B\right)$$
10	1 2 8 4 9	fmptdf2	$$⊢\phi \to \left(k\in A⟼B\right):A⟶\left[0,\mathrm{+\infty }\right]$$
11	7 3 10 5	xrge0tsmseq	$$⊢\phi \to C=\bigcup \left(\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left(k\in A⟼B\right)\right)$$
12	6 11	eqtr4id	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}B=C$$