# Metamath Proof Explorer

## Theorem elovolm

Description: Elementhood in the set M of approximations to the outer measure. (Contributed by Mario Carneiro, 16-Mar-2014)

Ref Expression
Hypothesis elovolm.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 elovolm ${⊢}{B}\in {M}↔\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 {B}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)\right)$

### Proof

Step Hyp Ref Expression
1 elovolm.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 eqeq1 ${⊢}{y}={B}\to \left({y}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)↔{B}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)\right)$
3 2 anbi2d ${⊢}{y}={B}\to \left(\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)↔\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {B}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)\right)\right)$
4 3 rexbidv ${⊢}{y}={B}\to \left(\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)↔\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 {B}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)\right)\right)$
5 4 1 elrab2 ${⊢}{B}\in {M}↔\left({B}\in {ℝ}^{*}\wedge \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 {B}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)\right)\right)$
6 elovolmlem ${⊢}{f}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)↔{f}:ℕ⟶\le \cap {ℝ}^{2}$
7 eqid ${⊢}\left(\mathrm{abs}\circ -\right)\circ {f}=\left(\mathrm{abs}\circ -\right)\circ {f}$
8 eqid ${⊢}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right)=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right)$
9 7 8 ovolsf ${⊢}{f}:ℕ⟶\le \cap {ℝ}^{2}\to seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right):ℕ⟶\left[0,\mathrm{+\infty }\right)$
10 6 9 sylbi ${⊢}{f}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\to seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right):ℕ⟶\left[0,\mathrm{+\infty }\right)$
11 icossxr ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq {ℝ}^{*}$
12 fss ${⊢}\left(seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right):ℕ⟶\left[0,\mathrm{+\infty }\right)\wedge \left[0,\mathrm{+\infty }\right)\subseteq {ℝ}^{*}\right)\to seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right):ℕ⟶{ℝ}^{*}$
13 10 11 12 sylancl ${⊢}{f}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\to seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right):ℕ⟶{ℝ}^{*}$
14 frn ${⊢}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right):ℕ⟶{ℝ}^{*}\to \mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right)\subseteq {ℝ}^{*}$
15 supxrcl ${⊢}\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right)\subseteq {ℝ}^{*}\to sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)\in {ℝ}^{*}$
16 13 14 15 3syl ${⊢}{f}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\to sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)\in {ℝ}^{*}$
17 eleq1 ${⊢}{B}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)\to \left({B}\in {ℝ}^{*}↔sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)\in {ℝ}^{*}\right)$
18 16 17 syl5ibrcom ${⊢}{f}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\to \left({B}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)\to {B}\in {ℝ}^{*}\right)$
19 18 imp ${⊢}\left({f}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\wedge {B}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)\right)\to {B}\in {ℝ}^{*}$
20 19 adantrl ${⊢}\left({f}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\wedge \left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge {B}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)\right)\right)\to {B}\in {ℝ}^{*}$
21 20 rexlimiva ${⊢}\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 {B}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)\right)\to {B}\in {ℝ}^{*}$
22 21 pm4.71ri ${⊢}\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 {B}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)\right)↔\left({B}\in {ℝ}^{*}\wedge \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 {B}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)\right)\right)$
23 5 22 bitr4i ${⊢}{B}\in {M}↔\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 {B}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)\right)$