Theorem esumex

Description: An extended sum is a set by definition. (Contributed by Thierry Arnoux, 5-Sep-2017)

	Ref	Expression
Assertion	esumex	$$⊢\underset{k\in A}{{\sum }^{*}}B\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		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)$$
2		ovex	$$⊢\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left(k\in A⟼B\right)\in \mathrm{V}$$
3	2	uniex	$$⊢\bigcup \left(\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left(k\in A⟼B\right)\right)\in \mathrm{V}$$
4	1 3	eqeltri	$$⊢\underset{k\in A}{{\sum }^{*}}B\in \mathrm{V}$$