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

Proof

Step	Hyp	Ref	Expression
1		ovolval.1	$$⊢M=\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		reex	$$⊢ℝ\in \mathrm{V}$$
3	2	elpw2	$$⊢A\in 𝒫ℝ\leftrightarrow 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)\leftrightarrow \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)}^{\mathbb{N}}\right)\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)\leftrightarrow \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)$$
6	5	rabbidv	$$⊢x=A\to \left\{y\in {ℝ}^{*}|\exists f\in \left({\left(\le \cap {ℝ}^2\right)}^{\mathbb{N}}\right)\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)}^{\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\}$$
7	6 1	eqtr4di	$$⊢x=A\to \left\{y\in {ℝ}^{*}|\exists f\in \left({\left(\le \cap {ℝ}^2\right)}^{\mathbb{N}}\right)\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 inf\left(\left\{y\in {ℝ}^{*}|\exists f\in \left({\left(\le \cap {ℝ}^2\right)}^{\mathbb{N}}\right)\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)=inf\left(M,{ℝ}^{*},<\right)$$
9		df-ovol	$$⊢{vol}^{*}=\left(x\in 𝒫ℝ⟼inf\left(\left\{y\in {ℝ}^{*}|\exists f\in \left({\left(\le \cap {ℝ}^2\right)}^{\mathbb{N}}\right)\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	$$⊢inf\left(M,{ℝ}^{*},<\right)\in \mathrm{V}$$
12	8 9 11	fvmpt	$$⊢A\in 𝒫ℝ\to {vol}^{*}\left(A\right)=inf\left(M,{ℝ}^{*},<\right)$$
13	3 12	sylbir	$$⊢A\subseteq ℝ\to {vol}^{*}\left(A\right)=inf\left(M,{ℝ}^{*},<\right)$$