# Metamath Proof Explorer

## Theorem ovnval

Description: Value of the Lebesgue outer measure for a given finite dimension. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypothesis ovnval.1 ${⊢}{\phi }\to {X}\in \mathrm{Fin}$
Assertion ovnval ${⊢}{\phi }\to \mathrm{voln*}\left({X}\right)=\left({y}\in 𝒫\left({ℝ}^{{X}}\right)⟼if\left({X}=\varnothing ,0,sup\left(\left\{{z}\in {ℝ}^{*}|\exists {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({y}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\wedge {z}=\mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)\right)\right)\right)\right\},{ℝ}^{*},<\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 ovnval.1 ${⊢}{\phi }\to {X}\in \mathrm{Fin}$
2 df-ovoln ${⊢}\mathrm{voln*}=\left({x}\in \mathrm{Fin}⟼\left({y}\in 𝒫\left({ℝ}^{{x}}\right)⟼if\left({x}=\varnothing ,0,sup\left(\left\{{z}\in {ℝ}^{*}|\exists {i}\in \left({\left({{ℝ}^{2}}^{{x}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({y}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {x}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\wedge {z}=\mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {x}}vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)\right)\right)\right)\right\},{ℝ}^{*},<\right)\right)\right)\right)$
3 oveq2 ${⊢}{x}={X}\to {ℝ}^{{x}}={ℝ}^{{X}}$
4 3 pweqd ${⊢}{x}={X}\to 𝒫\left({ℝ}^{{x}}\right)=𝒫\left({ℝ}^{{X}}\right)$
5 eqeq1 ${⊢}{x}={X}\to \left({x}=\varnothing ↔{X}=\varnothing \right)$
6 oveq2 ${⊢}{x}={X}\to {{ℝ}^{2}}^{{x}}={{ℝ}^{2}}^{{X}}$
7 6 oveq1d ${⊢}{x}={X}\to {\left({{ℝ}^{2}}^{{x}}\right)}^{ℕ}={\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}$
8 ixpeq1 ${⊢}{x}={X}\to \underset{{k}\in {x}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)=\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)$
9 8 iuneq2d ${⊢}{x}={X}\to \bigcup _{{j}\in ℕ}\underset{{k}\in {x}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)=\bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)$
10 9 sseq2d ${⊢}{x}={X}\to \left({y}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {x}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)↔{y}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)$
11 simpl ${⊢}\left({x}={X}\wedge {j}\in ℕ\right)\to {x}={X}$
12 11 prodeq1d ${⊢}\left({x}={X}\wedge {j}\in ℕ\right)\to \prod _{{k}\in {x}}vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)=\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)$
13 12 mpteq2dva ${⊢}{x}={X}\to \left({j}\in ℕ⟼\prod _{{k}\in {x}}vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)\right)=\left({j}\in ℕ⟼\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)\right)$
14 13 fveq2d ${⊢}{x}={X}\to \mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {x}}vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)\right)\right)=\mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)\right)\right)$
15 14 eqeq2d ${⊢}{x}={X}\to \left({z}=\mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {x}}vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)\right)\right)↔{z}=\mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)\right)\right)\right)$
16 10 15 anbi12d ${⊢}{x}={X}\to \left(\left({y}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {x}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\wedge {z}=\mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {x}}vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)\right)\right)\right)↔\left({y}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\wedge {z}=\mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)\right)\right)\right)\right)$
17 7 16 rexeqbidv ${⊢}{x}={X}\to \left(\exists {i}\in \left({\left({{ℝ}^{2}}^{{x}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({y}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {x}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\wedge {z}=\mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {x}}vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)\right)\right)\right)↔\exists {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({y}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\wedge {z}=\mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)\right)\right)\right)\right)$
18 17 rabbidv ${⊢}{x}={X}\to \left\{{z}\in {ℝ}^{*}|\exists {i}\in \left({\left({{ℝ}^{2}}^{{x}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({y}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {x}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\wedge {z}=\mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {x}}vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)\right)\right)\right)\right\}=\left\{{z}\in {ℝ}^{*}|\exists {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({y}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\wedge {z}=\mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)\right)\right)\right)\right\}$
19 18 infeq1d ${⊢}{x}={X}\to sup\left(\left\{{z}\in {ℝ}^{*}|\exists {i}\in \left({\left({{ℝ}^{2}}^{{x}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({y}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {x}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\wedge {z}=\mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {x}}vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)\right)\right)\right)\right\},{ℝ}^{*},<\right)=sup\left(\left\{{z}\in {ℝ}^{*}|\exists {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({y}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\wedge {z}=\mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)\right)\right)\right)\right\},{ℝ}^{*},<\right)$
20 5 19 ifbieq2d ${⊢}{x}={X}\to if\left({x}=\varnothing ,0,sup\left(\left\{{z}\in {ℝ}^{*}|\exists {i}\in \left({\left({{ℝ}^{2}}^{{x}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({y}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {x}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\wedge {z}=\mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {x}}vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)\right)\right)\right)\right\},{ℝ}^{*},<\right)\right)=if\left({X}=\varnothing ,0,sup\left(\left\{{z}\in {ℝ}^{*}|\exists {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({y}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\wedge {z}=\mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)\right)\right)\right)\right\},{ℝ}^{*},<\right)\right)$
21 4 20 mpteq12dv ${⊢}{x}={X}\to \left({y}\in 𝒫\left({ℝ}^{{x}}\right)⟼if\left({x}=\varnothing ,0,sup\left(\left\{{z}\in {ℝ}^{*}|\exists {i}\in \left({\left({{ℝ}^{2}}^{{x}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({y}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {x}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\wedge {z}=\mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {x}}vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)\right)\right)\right)\right\},{ℝ}^{*},<\right)\right)\right)=\left({y}\in 𝒫\left({ℝ}^{{X}}\right)⟼if\left({X}=\varnothing ,0,sup\left(\left\{{z}\in {ℝ}^{*}|\exists {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({y}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\wedge {z}=\mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)\right)\right)\right)\right\},{ℝ}^{*},<\right)\right)\right)$
22 ovex ${⊢}{ℝ}^{{X}}\in \mathrm{V}$
23 22 pwex ${⊢}𝒫\left({ℝ}^{{X}}\right)\in \mathrm{V}$
24 23 mptex ${⊢}\left({y}\in 𝒫\left({ℝ}^{{X}}\right)⟼if\left({X}=\varnothing ,0,sup\left(\left\{{z}\in {ℝ}^{*}|\exists {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({y}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\wedge {z}=\mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)\right)\right)\right)\right\},{ℝ}^{*},<\right)\right)\right)\in \mathrm{V}$
25 24 a1i ${⊢}{\phi }\to \left({y}\in 𝒫\left({ℝ}^{{X}}\right)⟼if\left({X}=\varnothing ,0,sup\left(\left\{{z}\in {ℝ}^{*}|\exists {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({y}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\wedge {z}=\mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)\right)\right)\right)\right\},{ℝ}^{*},<\right)\right)\right)\in \mathrm{V}$
26 2 21 1 25 fvmptd3 ${⊢}{\phi }\to \mathrm{voln*}\left({X}\right)=\left({y}\in 𝒫\left({ℝ}^{{X}}\right)⟼if\left({X}=\varnothing ,0,sup\left(\left\{{z}\in {ℝ}^{*}|\exists {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({y}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\wedge {z}=\mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)\right)\right)\right)\right\},{ℝ}^{*},<\right)\right)\right)$