Theorem ovolss

Description: The volume of a set is monotone with respect to set inclusion. (Contributed by Mario Carneiro, 16-Mar-2014)

	Ref	Expression
Assertion	ovolss	$$⊢\left(A\subseteq B\wedge B\subseteq ℝ\right)\to {vol}^{*}\left(A\right)\le {vol}^{*}\left(B\right)$$

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		eqid	$$⊢\left\{y\in {ℝ}^{*}|\exists f\in \left({\left(\le \cap {ℝ}^2\right)}^{\mathbb{N}}\right)\left(B\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(B\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\}$$
3	1 2	ovolsslem	$$⊢\left(A\subseteq B\wedge B\subseteq ℝ\right)\to {vol}^{*}\left(A\right)\le {vol}^{*}\left(B\right)$$