Theorem ovolcl

Description: The volume of a set is an extended real number. (Contributed by Mario Carneiro, 16-Mar-2014)

	Ref	Expression
Assertion	ovolcl	$$⊢A\subseteq ℝ\to {vol}^{*}\left(A\right)\in {ℝ}^{*}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left\{y\in {ℝ}^{*}|\exists f\in \left({\left(\le \cap {ℝ}^2\right)}^{\mathbb{N}}\right)\left(A\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ f\right)\wedge y=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ f\right)\right),{ℝ}^{*},<\right)\right)\right\}=\left\{y\in {ℝ}^{*}|\exists f\in \left({\left(\le \cap {ℝ}^2\right)}^{\mathbb{N}}\right)\left(A\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ f\right)\wedge y=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ f\right)\right),{ℝ}^{*},<\right)\right)\right\}$$
2	1	ovolval	$$⊢A\subseteq ℝ\to {vol}^{*}\left(A\right)=inf\left(\left\{y\in {ℝ}^{*}|\exists f\in \left({\left(\le \cap {ℝ}^2\right)}^{\mathbb{N}}\right)\left(A\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ f\right)\wedge y=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ f\right)\right),{ℝ}^{*},<\right)\right)\right\},{ℝ}^{*},<\right)$$
3		ssrab2	$$⊢\left\{y\in {ℝ}^{*}|\exists f\in \left({\left(\le \cap {ℝ}^2\right)}^{\mathbb{N}}\right)\left(A\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ f\right)\wedge y=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ f\right)\right),{ℝ}^{*},<\right)\right)\right\}\subseteq {ℝ}^{*}$$
4		infxrcl	$$⊢\left\{y\in {ℝ}^{*}|\exists f\in \left({\left(\le \cap {ℝ}^2\right)}^{\mathbb{N}}\right)\left(A\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ f\right)\wedge y=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ f\right)\right),{ℝ}^{*},<\right)\right)\right\}\subseteq {ℝ}^{*}\to inf\left(\left\{y\in {ℝ}^{*}|\exists f\in \left({\left(\le \cap {ℝ}^2\right)}^{\mathbb{N}}\right)\left(A\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ f\right)\wedge y=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ f\right)\right),{ℝ}^{*},<\right)\right)\right\},{ℝ}^{*},<\right)\in {ℝ}^{*}$$
5	3 4	ax-mp	$$⊢inf\left(\left\{y\in {ℝ}^{*}|\exists f\in \left({\left(\le \cap {ℝ}^2\right)}^{\mathbb{N}}\right)\left(A\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ f\right)\wedge y=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ f\right)\right),{ℝ}^{*},<\right)\right)\right\},{ℝ}^{*},<\right)\in {ℝ}^{*}$$
6	2 5	eqeltrdi	$$⊢A\subseteq ℝ\to {vol}^{*}\left(A\right)\in {ℝ}^{*}$$