# Metamath Proof Explorer

## Theorem ovolge0

Description: The volume of a set is always nonnegative. (Contributed by Mario Carneiro, 16-Mar-2014)

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

### Proof

Step Hyp Ref Expression
1 ssrab2 ${⊢}\left\{{y}\in {ℝ}^{*}|\exists {f}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\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 {ℝ}^{*}$
2 0xr ${⊢}0\in {ℝ}^{*}$
3 infxrgelb ${⊢}\left(\left\{{y}\in {ℝ}^{*}|\exists {f}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\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 {ℝ}^{*}\wedge 0\in {ℝ}^{*}\right)\to \left(0\le sup\left(\left\{{y}\in {ℝ}^{*}|\exists {f}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\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)↔\forall {x}\in \left\{{y}\in {ℝ}^{*}|\exists {f}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\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\}\phantom{\rule{.4em}{0ex}}0\le {x}\right)$
4 1 2 3 mp2an ${⊢}0\le sup\left(\left\{{y}\in {ℝ}^{*}|\exists {f}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\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)↔\forall {x}\in \left\{{y}\in {ℝ}^{*}|\exists {f}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\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\}\phantom{\rule{.4em}{0ex}}0\le {x}$
5 eqid ${⊢}\left\{{y}\in {ℝ}^{*}|\exists {f}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\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)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\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\}$
6 5 ovolmge0 ${⊢}{x}\in \left\{{y}\in {ℝ}^{*}|\exists {f}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\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\}\to 0\le {x}$
7 4 6 mprgbir ${⊢}0\le sup\left(\left\{{y}\in {ℝ}^{*}|\exists {f}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\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)$
8 5 ovolval ${⊢}{A}\subseteq ℝ\to {vol}^{*}\left({A}\right)=sup\left(\left\{{y}\in {ℝ}^{*}|\exists {f}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\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)$
9 7 8 breqtrrid ${⊢}{A}\subseteq ℝ\to 0\le {vol}^{*}\left({A}\right)$