# Metamath Proof Explorer

## Theorem ovollb

Description: The outer volume is a lower bound on the sum of all interval coverings of A . (Contributed by Mario Carneiro, 15-Jun-2014)

Ref Expression
Hypothesis ovollb.1 ${⊢}{S}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\right)\right)$
Assertion ovollb ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\to {vol}^{*}\left({A}\right)\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)$

### Proof

Step Hyp Ref Expression
1 ovollb.1 ${⊢}{S}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\right)\right)$
2 simpr ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\to {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)$
3 ioof ${⊢}\left(.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫ℝ$
4 simpl ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\to {F}:ℕ⟶\le \cap {ℝ}^{2}$
5 inss2 ${⊢}\le \cap {ℝ}^{2}\subseteq {ℝ}^{2}$
6 rexpssxrxp ${⊢}{ℝ}^{2}\subseteq {ℝ}^{*}×{ℝ}^{*}$
7 5 6 sstri ${⊢}\le \cap {ℝ}^{2}\subseteq {ℝ}^{*}×{ℝ}^{*}$
8 fss ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge \le \cap {ℝ}^{2}\subseteq {ℝ}^{*}×{ℝ}^{*}\right)\to {F}:ℕ⟶{ℝ}^{*}×{ℝ}^{*}$
9 4 7 8 sylancl ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\to {F}:ℕ⟶{ℝ}^{*}×{ℝ}^{*}$
10 fco ${⊢}\left(\left(.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫ℝ\wedge {F}:ℕ⟶{ℝ}^{*}×{ℝ}^{*}\right)\to \left(\left(.\right)\circ {F}\right):ℕ⟶𝒫ℝ$
11 3 9 10 sylancr ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\to \left(\left(.\right)\circ {F}\right):ℕ⟶𝒫ℝ$
12 11 frnd ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\to \mathrm{ran}\left(\left(.\right)\circ {F}\right)\subseteq 𝒫ℝ$
13 sspwuni ${⊢}\mathrm{ran}\left(\left(.\right)\circ {F}\right)\subseteq 𝒫ℝ↔\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\subseteq ℝ$
14 12 13 sylib ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\to \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\subseteq ℝ$
15 2 14 sstrd ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\to {A}\subseteq ℝ$
16 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\}$
17 16 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)$
18 15 17 syl ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\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)$
19 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 {ℝ}^{*}$
20 16 1 elovolmr ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\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\}$
21 infxrlb ${⊢}\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 sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\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\}\right)\to 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)\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)$
22 19 20 21 sylancr ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\to 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)\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)$
23 18 22 eqbrtrd ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\to {vol}^{*}\left({A}\right)\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)$