# Metamath Proof Explorer

## Theorem ovolfioo

Description: Unpack the interval covering property of the outer measure definition. (Contributed by Mario Carneiro, 16-Mar-2014)

Ref Expression
Assertion ovolfioo ${⊢}\left({A}\subseteq ℝ\wedge {F}:ℕ⟶\le \cap {ℝ}^{2}\right)\to \left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)↔\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({F}\left({n}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({F}\left({n}\right)\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 ioof ${⊢}\left(.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫ℝ$
2 inss2 ${⊢}\le \cap {ℝ}^{2}\subseteq {ℝ}^{2}$
3 rexpssxrxp ${⊢}{ℝ}^{2}\subseteq {ℝ}^{*}×{ℝ}^{*}$
4 2 3 sstri ${⊢}\le \cap {ℝ}^{2}\subseteq {ℝ}^{*}×{ℝ}^{*}$
5 fss ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge \le \cap {ℝ}^{2}\subseteq {ℝ}^{*}×{ℝ}^{*}\right)\to {F}:ℕ⟶{ℝ}^{*}×{ℝ}^{*}$
6 4 5 mpan2 ${⊢}{F}:ℕ⟶\le \cap {ℝ}^{2}\to {F}:ℕ⟶{ℝ}^{*}×{ℝ}^{*}$
7 fco ${⊢}\left(\left(.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫ℝ\wedge {F}:ℕ⟶{ℝ}^{*}×{ℝ}^{*}\right)\to \left(\left(.\right)\circ {F}\right):ℕ⟶𝒫ℝ$
8 1 6 7 sylancr ${⊢}{F}:ℕ⟶\le \cap {ℝ}^{2}\to \left(\left(.\right)\circ {F}\right):ℕ⟶𝒫ℝ$
9 ffn ${⊢}\left(\left(.\right)\circ {F}\right):ℕ⟶𝒫ℝ\to \left(\left(.\right)\circ {F}\right)Fnℕ$
10 fniunfv ${⊢}\left(\left(.\right)\circ {F}\right)Fnℕ\to \bigcup _{{n}\in ℕ}\left(\left(.\right)\circ {F}\right)\left({n}\right)=\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)$
11 8 9 10 3syl ${⊢}{F}:ℕ⟶\le \cap {ℝ}^{2}\to \bigcup _{{n}\in ℕ}\left(\left(.\right)\circ {F}\right)\left({n}\right)=\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)$
12 11 sseq2d ${⊢}{F}:ℕ⟶\le \cap {ℝ}^{2}\to \left({A}\subseteq \bigcup _{{n}\in ℕ}\left(\left(.\right)\circ {F}\right)\left({n}\right)↔{A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)$
13 12 adantl ${⊢}\left({A}\subseteq ℝ\wedge {F}:ℕ⟶\le \cap {ℝ}^{2}\right)\to \left({A}\subseteq \bigcup _{{n}\in ℕ}\left(\left(.\right)\circ {F}\right)\left({n}\right)↔{A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)$
14 dfss3 ${⊢}{A}\subseteq \bigcup _{{n}\in ℕ}\left(\left(.\right)\circ {F}\right)\left({n}\right)↔\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}\in \bigcup _{{n}\in ℕ}\left(\left(.\right)\circ {F}\right)\left({n}\right)$
15 ssel2 ${⊢}\left({A}\subseteq ℝ\wedge {z}\in {A}\right)\to {z}\in ℝ$
16 eliun ${⊢}{z}\in \bigcup _{{n}\in ℕ}\left(\left(.\right)\circ {F}\right)\left({n}\right)↔\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{z}\in \left(\left(.\right)\circ {F}\right)\left({n}\right)$
17 rexr ${⊢}{z}\in ℝ\to {z}\in {ℝ}^{*}$
18 17 ad2antrr ${⊢}\left(\left({z}\in ℝ\wedge {F}:ℕ⟶\le \cap {ℝ}^{2}\right)\wedge {n}\in ℕ\right)\to {z}\in {ℝ}^{*}$
19 fvco3 ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {n}\in ℕ\right)\to \left(\left(.\right)\circ {F}\right)\left({n}\right)=\left(.\right)\left({F}\left({n}\right)\right)$
20 ffvelrn ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {n}\in ℕ\right)\to {F}\left({n}\right)\in \left(\le \cap {ℝ}^{2}\right)$
21 20 elin2d ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {n}\in ℕ\right)\to {F}\left({n}\right)\in {ℝ}^{2}$
22 1st2nd2 ${⊢}{F}\left({n}\right)\in {ℝ}^{2}\to {F}\left({n}\right)=⟨{1}^{st}\left({F}\left({n}\right)\right),{2}^{nd}\left({F}\left({n}\right)\right)⟩$
23 21 22 syl ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {n}\in ℕ\right)\to {F}\left({n}\right)=⟨{1}^{st}\left({F}\left({n}\right)\right),{2}^{nd}\left({F}\left({n}\right)\right)⟩$
24 23 fveq2d ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {n}\in ℕ\right)\to \left(.\right)\left({F}\left({n}\right)\right)=\left(.\right)\left(⟨{1}^{st}\left({F}\left({n}\right)\right),{2}^{nd}\left({F}\left({n}\right)\right)⟩\right)$
25 df-ov ${⊢}\left({1}^{st}\left({F}\left({n}\right)\right),{2}^{nd}\left({F}\left({n}\right)\right)\right)=\left(.\right)\left(⟨{1}^{st}\left({F}\left({n}\right)\right),{2}^{nd}\left({F}\left({n}\right)\right)⟩\right)$
26 24 25 syl6eqr ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {n}\in ℕ\right)\to \left(.\right)\left({F}\left({n}\right)\right)=\left({1}^{st}\left({F}\left({n}\right)\right),{2}^{nd}\left({F}\left({n}\right)\right)\right)$
27 19 26 eqtrd ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {n}\in ℕ\right)\to \left(\left(.\right)\circ {F}\right)\left({n}\right)=\left({1}^{st}\left({F}\left({n}\right)\right),{2}^{nd}\left({F}\left({n}\right)\right)\right)$
28 27 eleq2d ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {n}\in ℕ\right)\to \left({z}\in \left(\left(.\right)\circ {F}\right)\left({n}\right)↔{z}\in \left({1}^{st}\left({F}\left({n}\right)\right),{2}^{nd}\left({F}\left({n}\right)\right)\right)\right)$
29 ovolfcl ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {n}\in ℕ\right)\to \left({1}^{st}\left({F}\left({n}\right)\right)\in ℝ\wedge {2}^{nd}\left({F}\left({n}\right)\right)\in ℝ\wedge {1}^{st}\left({F}\left({n}\right)\right)\le {2}^{nd}\left({F}\left({n}\right)\right)\right)$
30 rexr ${⊢}{1}^{st}\left({F}\left({n}\right)\right)\in ℝ\to {1}^{st}\left({F}\left({n}\right)\right)\in {ℝ}^{*}$
31 rexr ${⊢}{2}^{nd}\left({F}\left({n}\right)\right)\in ℝ\to {2}^{nd}\left({F}\left({n}\right)\right)\in {ℝ}^{*}$
32 elioo1 ${⊢}\left({1}^{st}\left({F}\left({n}\right)\right)\in {ℝ}^{*}\wedge {2}^{nd}\left({F}\left({n}\right)\right)\in {ℝ}^{*}\right)\to \left({z}\in \left({1}^{st}\left({F}\left({n}\right)\right),{2}^{nd}\left({F}\left({n}\right)\right)\right)↔\left({z}\in {ℝ}^{*}\wedge {1}^{st}\left({F}\left({n}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({F}\left({n}\right)\right)\right)\right)$
33 30 31 32 syl2an ${⊢}\left({1}^{st}\left({F}\left({n}\right)\right)\in ℝ\wedge {2}^{nd}\left({F}\left({n}\right)\right)\in ℝ\right)\to \left({z}\in \left({1}^{st}\left({F}\left({n}\right)\right),{2}^{nd}\left({F}\left({n}\right)\right)\right)↔\left({z}\in {ℝ}^{*}\wedge {1}^{st}\left({F}\left({n}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({F}\left({n}\right)\right)\right)\right)$
34 3anass ${⊢}\left({z}\in {ℝ}^{*}\wedge {1}^{st}\left({F}\left({n}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({F}\left({n}\right)\right)\right)↔\left({z}\in {ℝ}^{*}\wedge \left({1}^{st}\left({F}\left({n}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({F}\left({n}\right)\right)\right)\right)$
35 33 34 syl6bb ${⊢}\left({1}^{st}\left({F}\left({n}\right)\right)\in ℝ\wedge {2}^{nd}\left({F}\left({n}\right)\right)\in ℝ\right)\to \left({z}\in \left({1}^{st}\left({F}\left({n}\right)\right),{2}^{nd}\left({F}\left({n}\right)\right)\right)↔\left({z}\in {ℝ}^{*}\wedge \left({1}^{st}\left({F}\left({n}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({F}\left({n}\right)\right)\right)\right)\right)$
36 35 3adant3 ${⊢}\left({1}^{st}\left({F}\left({n}\right)\right)\in ℝ\wedge {2}^{nd}\left({F}\left({n}\right)\right)\in ℝ\wedge {1}^{st}\left({F}\left({n}\right)\right)\le {2}^{nd}\left({F}\left({n}\right)\right)\right)\to \left({z}\in \left({1}^{st}\left({F}\left({n}\right)\right),{2}^{nd}\left({F}\left({n}\right)\right)\right)↔\left({z}\in {ℝ}^{*}\wedge \left({1}^{st}\left({F}\left({n}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({F}\left({n}\right)\right)\right)\right)\right)$
37 29 36 syl ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {n}\in ℕ\right)\to \left({z}\in \left({1}^{st}\left({F}\left({n}\right)\right),{2}^{nd}\left({F}\left({n}\right)\right)\right)↔\left({z}\in {ℝ}^{*}\wedge \left({1}^{st}\left({F}\left({n}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({F}\left({n}\right)\right)\right)\right)\right)$
38 28 37 bitrd ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {n}\in ℕ\right)\to \left({z}\in \left(\left(.\right)\circ {F}\right)\left({n}\right)↔\left({z}\in {ℝ}^{*}\wedge \left({1}^{st}\left({F}\left({n}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({F}\left({n}\right)\right)\right)\right)\right)$
39 38 adantll ${⊢}\left(\left({z}\in ℝ\wedge {F}:ℕ⟶\le \cap {ℝ}^{2}\right)\wedge {n}\in ℕ\right)\to \left({z}\in \left(\left(.\right)\circ {F}\right)\left({n}\right)↔\left({z}\in {ℝ}^{*}\wedge \left({1}^{st}\left({F}\left({n}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({F}\left({n}\right)\right)\right)\right)\right)$
40 18 39 mpbirand ${⊢}\left(\left({z}\in ℝ\wedge {F}:ℕ⟶\le \cap {ℝ}^{2}\right)\wedge {n}\in ℕ\right)\to \left({z}\in \left(\left(.\right)\circ {F}\right)\left({n}\right)↔\left({1}^{st}\left({F}\left({n}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({F}\left({n}\right)\right)\right)\right)$
41 40 rexbidva ${⊢}\left({z}\in ℝ\wedge {F}:ℕ⟶\le \cap {ℝ}^{2}\right)\to \left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{z}\in \left(\left(.\right)\circ {F}\right)\left({n}\right)↔\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({F}\left({n}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({F}\left({n}\right)\right)\right)\right)$
42 16 41 syl5bb ${⊢}\left({z}\in ℝ\wedge {F}:ℕ⟶\le \cap {ℝ}^{2}\right)\to \left({z}\in \bigcup _{{n}\in ℕ}\left(\left(.\right)\circ {F}\right)\left({n}\right)↔\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({F}\left({n}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({F}\left({n}\right)\right)\right)\right)$
43 15 42 sylan ${⊢}\left(\left({A}\subseteq ℝ\wedge {z}\in {A}\right)\wedge {F}:ℕ⟶\le \cap {ℝ}^{2}\right)\to \left({z}\in \bigcup _{{n}\in ℕ}\left(\left(.\right)\circ {F}\right)\left({n}\right)↔\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({F}\left({n}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({F}\left({n}\right)\right)\right)\right)$
44 43 an32s ${⊢}\left(\left({A}\subseteq ℝ\wedge {F}:ℕ⟶\le \cap {ℝ}^{2}\right)\wedge {z}\in {A}\right)\to \left({z}\in \bigcup _{{n}\in ℕ}\left(\left(.\right)\circ {F}\right)\left({n}\right)↔\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({F}\left({n}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({F}\left({n}\right)\right)\right)\right)$
45 44 ralbidva ${⊢}\left({A}\subseteq ℝ\wedge {F}:ℕ⟶\le \cap {ℝ}^{2}\right)\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}\in \bigcup _{{n}\in ℕ}\left(\left(.\right)\circ {F}\right)\left({n}\right)↔\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({F}\left({n}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({F}\left({n}\right)\right)\right)\right)$
46 14 45 syl5bb ${⊢}\left({A}\subseteq ℝ\wedge {F}:ℕ⟶\le \cap {ℝ}^{2}\right)\to \left({A}\subseteq \bigcup _{{n}\in ℕ}\left(\left(.\right)\circ {F}\right)\left({n}\right)↔\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({F}\left({n}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({F}\left({n}\right)\right)\right)\right)$
47 13 46 bitr3d ${⊢}\left({A}\subseteq ℝ\wedge {F}:ℕ⟶\le \cap {ℝ}^{2}\right)\to \left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)↔\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({F}\left({n}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({F}\left({n}\right)\right)\right)\right)$