# Metamath Proof Explorer

## Theorem ovolval

Description: The value of the outer measure. (Contributed by Mario Carneiro, 16-Mar-2014) (Revised by AV, 17-Sep-2020)

Ref Expression
Hypothesis ovolval.1 ${⊢}{M}=\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\}$
Assertion ovolval ${⊢}{A}\subseteq ℝ\to {vol}^{*}\left({A}\right)=sup\left({M},{ℝ}^{*},<\right)$

### Proof

Step Hyp Ref Expression
1 ovolval.1 ${⊢}{M}=\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\}$
2 reex ${⊢}ℝ\in \mathrm{V}$
3 2 elpw2 ${⊢}{A}\in 𝒫ℝ↔{A}\subseteq ℝ$
4 cleq1lem ${⊢}{x}={A}\to \left(\left({x}\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)↔\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)$
5 4 rexbidv ${⊢}{x}={A}\to \left(\exists {f}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({x}\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)↔\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 rabbidv ${⊢}{x}={A}\to \left\{{y}\in {ℝ}^{*}|\exists {f}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({x}\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\}$
7 6 1 eqtr4di ${⊢}{x}={A}\to \left\{{y}\in {ℝ}^{*}|\exists {f}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({x}\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\}={M}$
8 7 infeq1d ${⊢}{x}={A}\to sup\left(\left\{{y}\in {ℝ}^{*}|\exists {f}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({x}\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)=sup\left({M},{ℝ}^{*},<\right)$
9 df-ovol ${⊢}{vol}^{*}=\left({x}\in 𝒫ℝ⟼sup\left(\left\{{y}\in {ℝ}^{*}|\exists {f}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({x}\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)\right)$
10 xrltso ${⊢}<\mathrm{Or}{ℝ}^{*}$
11 10 infex ${⊢}sup\left({M},{ℝ}^{*},<\right)\in \mathrm{V}$
12 8 9 11 fvmpt ${⊢}{A}\in 𝒫ℝ\to {vol}^{*}\left({A}\right)=sup\left({M},{ℝ}^{*},<\right)$
13 3 12 sylbir ${⊢}{A}\subseteq ℝ\to {vol}^{*}\left({A}\right)=sup\left({M},{ℝ}^{*},<\right)$