Theorem ovolval4

Description: The value of the Lebesgue outer measure for subsets of the reals. Similar to ovolval3 , but here f may represent unordered interval bounds. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	ovolval4.a	$$⊢\phi \to A\subseteq ℝ$$
	ovolval4.m	$$⊢M=\left\{y\in {ℝ}^{*}|\exists f\in \left({{ℝ}^2}^{\mathbb{N}}\right)\left(A\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ f\right)\wedge y=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ f\right)\right)\right\}$$
Assertion	ovolval4	$$⊢\phi \to {vol}^{*}\left(A\right)=inf\left(M,{ℝ}^{*},<\right)$$

Proof

Step	Hyp	Ref	Expression
1		ovolval4.a	$$⊢\phi \to A\subseteq ℝ$$
2		ovolval4.m	$$⊢M=\left\{y\in {ℝ}^{*}|\exists f\in \left({{ℝ}^2}^{\mathbb{N}}\right)\left(A\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ f\right)\wedge y=\mathrm{sum^}\left(\left(vol\circ \left(.\right)\right)\circ f\right)\right)\right\}$$
3		2fveq3	$$⊢k=n\to 1^{st}\left(f\left(k\right)\right)=1^{st}\left(f\left(n\right)\right)$$
4		2fveq3	$$⊢k=n\to 2^{nd}\left(f\left(k\right)\right)=2^{nd}\left(f\left(n\right)\right)$$
5	3 4	breq12d	$$⊢k=n\to \left(1^{st}\left(f\left(k\right)\right)\le 2^{nd}\left(f\left(k\right)\right)\leftrightarrow 1^{st}\left(f\left(n\right)\right)\le 2^{nd}\left(f\left(n\right)\right)\right)$$
6	5 4 3	ifbieq12d	$$⊢k=n\to if\left(1^{st}\left(f\left(k\right)\right)\le 2^{nd}\left(f\left(k\right)\right),2^{nd}\left(f\left(k\right)\right),1^{st}\left(f\left(k\right)\right)\right)=if\left(1^{st}\left(f\left(n\right)\right)\le 2^{nd}\left(f\left(n\right)\right),2^{nd}\left(f\left(n\right)\right),1^{st}\left(f\left(n\right)\right)\right)$$
7	3 6	opeq12d	$$⊢k=n\to ⟨1^{st}\left(f\left(k\right)\right),if\left(1^{st}\left(f\left(k\right)\right)\le 2^{nd}\left(f\left(k\right)\right),2^{nd}\left(f\left(k\right)\right),1^{st}\left(f\left(k\right)\right)\right)⟩=⟨1^{st}\left(f\left(n\right)\right),if\left(1^{st}\left(f\left(n\right)\right)\le 2^{nd}\left(f\left(n\right)\right),2^{nd}\left(f\left(n\right)\right),1^{st}\left(f\left(n\right)\right)\right)⟩$$
8	7	cbvmptv	$$⊢\left(k\in \mathbb{N}⟼⟨1^{st}\left(f\left(k\right)\right),if\left(1^{st}\left(f\left(k\right)\right)\le 2^{nd}\left(f\left(k\right)\right),2^{nd}\left(f\left(k\right)\right),1^{st}\left(f\left(k\right)\right)\right)⟩\right)=\left(n\in \mathbb{N}⟼⟨1^{st}\left(f\left(n\right)\right),if\left(1^{st}\left(f\left(n\right)\right)\le 2^{nd}\left(f\left(n\right)\right),2^{nd}\left(f\left(n\right)\right),1^{st}\left(f\left(n\right)\right)\right)⟩\right)$$
9	1 2 8	ovolval4lem2	$$⊢\phi \to {vol}^{*}\left(A\right)=inf\left(M,{ℝ}^{*},<\right)$$