Metamath Proof Explorer

Theorem ovncvrrp

Description: The Lebesgue outer measure of a subset of multidimensional real numbers can always be approximated by the total outer measure of a cover of half-open (multidimensional) intervals. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses ovncvrrp.x ${⊢}{\phi }\to {X}\in \mathrm{Fin}$
ovncvrrp.n0 ${⊢}{\phi }\to {X}\ne \varnothing$
ovncvrrp.a ${⊢}{\phi }\to {A}\subseteq {ℝ}^{{X}}$
ovncvrrp.e ${⊢}{\phi }\to {E}\in {ℝ}^{+}$
ovncvrrp.c ${⊢}{C}=\left({a}\in 𝒫\left({ℝ}^{{X}}\right)⟼\left\{{l}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)|{a}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {l}\left({j}\right)\right)\left({k}\right)\right\}\right)$
ovncvrrp.l ${⊢}{L}=\left({h}\in \left({{ℝ}^{2}}^{{X}}\right)⟼\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {h}\right)\left({k}\right)\right)\right)$
ovncvrrp.d ${⊢}{D}=\left({a}\in 𝒫\left({ℝ}^{{X}}\right)⟼\left({e}\in {ℝ}^{+}⟼\left\{{i}\in {C}\left({a}\right)|\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({a}\right){+}_{𝑒}{e}\right\}\right)\right)$
Assertion ovncvrrp ${⊢}{\phi }\to \exists {i}\phantom{\rule{.4em}{0ex}}{i}\in {D}\left({A}\right)\left({E}\right)$

Proof

Step Hyp Ref Expression
1 ovncvrrp.x ${⊢}{\phi }\to {X}\in \mathrm{Fin}$
2 ovncvrrp.n0 ${⊢}{\phi }\to {X}\ne \varnothing$
3 ovncvrrp.a ${⊢}{\phi }\to {A}\subseteq {ℝ}^{{X}}$
4 ovncvrrp.e ${⊢}{\phi }\to {E}\in {ℝ}^{+}$
5 ovncvrrp.c ${⊢}{C}=\left({a}\in 𝒫\left({ℝ}^{{X}}\right)⟼\left\{{l}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)|{a}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {l}\left({j}\right)\right)\left({k}\right)\right\}\right)$
6 ovncvrrp.l ${⊢}{L}=\left({h}\in \left({{ℝ}^{2}}^{{X}}\right)⟼\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {h}\right)\left({k}\right)\right)\right)$
7 ovncvrrp.d ${⊢}{D}=\left({a}\in 𝒫\left({ℝ}^{{X}}\right)⟼\left({e}\in {ℝ}^{+}⟼\left\{{i}\in {C}\left({a}\right)|\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({a}\right){+}_{𝑒}{e}\right\}\right)\right)$
8 eqid ${⊢}\left\{{z}\in {ℝ}^{*}|\exists {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\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({A}\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\}$
9 1 2 3 4 8 ovnlerp ${⊢}{\phi }\to \exists {z}\in \left\{{z}\in {ℝ}^{*}|\exists {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\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\}\phantom{\rule{.4em}{0ex}}{z}\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}$
10 simp1 ${⊢}\left({\phi }\wedge {z}\in \left\{{z}\in {ℝ}^{*}|\exists {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\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\}\wedge {z}\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\to {\phi }$
11 simp3 ${⊢}\left({\phi }\wedge {z}\in \left\{{z}\in {ℝ}^{*}|\exists {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\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\}\wedge {z}\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\to {z}\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}$
12 rabid ${⊢}{z}\in \left\{{z}\in {ℝ}^{*}|\exists {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\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 {ℝ}^{*}\wedge \exists {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\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)$
13 12 biimpi ${⊢}{z}\in \left\{{z}\in {ℝ}^{*}|\exists {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\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\}\to \left({z}\in {ℝ}^{*}\wedge \exists {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\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)$
14 13 simprd ${⊢}{z}\in \left\{{z}\in {ℝ}^{*}|\exists {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\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\}\to \exists {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\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)$
15 14 adantr ${⊢}\left({z}\in \left\{{z}\in {ℝ}^{*}|\exists {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\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\}\wedge {z}\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\to \exists {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\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)$
16 15 3adant1 ${⊢}\left({\phi }\wedge {z}\in \left\{{z}\in {ℝ}^{*}|\exists {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\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\}\wedge {z}\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\to \exists {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\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)$
17 nfv ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {z}\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)$
18 nfe1 ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}\exists {i}\phantom{\rule{.4em}{0ex}}\left({i}\in {C}\left({A}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)$
19 simp1l ${⊢}\left(\left({\phi }\wedge {z}\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\wedge {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\wedge \left({A}\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)\to {\phi }$
20 simp2 ${⊢}\left(\left({\phi }\wedge {z}\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\wedge {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\wedge \left({A}\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)\to {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)$
21 simp3l ${⊢}\left(\left({\phi }\wedge {z}\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\wedge {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\wedge \left({A}\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)\to {A}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)$
22 id ${⊢}\left({i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\wedge {A}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)\to \left({i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\wedge {A}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)$
23 fveq1 ${⊢}{l}={i}\to {l}\left({j}\right)={i}\left({j}\right)$
24 23 coeq2d ${⊢}{l}={i}\to \left[.\right)\circ {l}\left({j}\right)=\left[.\right)\circ {i}\left({j}\right)$
25 24 fveq1d ${⊢}{l}={i}\to \left(\left[.\right)\circ {l}\left({j}\right)\right)\left({k}\right)=\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)$
26 25 ixpeq2dv ${⊢}{l}={i}\to \underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {l}\left({j}\right)\right)\left({k}\right)=\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)$
27 26 iuneq2d ${⊢}{l}={i}\to \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {l}\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)$
28 27 sseq2d ${⊢}{l}={i}\to \left({A}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {l}\left({j}\right)\right)\left({k}\right)↔{A}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)$
29 28 elrab ${⊢}{i}\in \left\{{l}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)|{A}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {l}\left({j}\right)\right)\left({k}\right)\right\}↔\left({i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\wedge {A}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)$
30 22 29 sylibr ${⊢}\left({i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\wedge {A}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)\to {i}\in \left\{{l}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)|{A}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {l}\left({j}\right)\right)\left({k}\right)\right\}$
31 30 3adant1 ${⊢}\left({\phi }\wedge {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\wedge {A}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)\to {i}\in \left\{{l}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)|{A}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {l}\left({j}\right)\right)\left({k}\right)\right\}$
32 sseq1 ${⊢}{a}={A}\to \left({a}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {l}\left({j}\right)\right)\left({k}\right)↔{A}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {l}\left({j}\right)\right)\left({k}\right)\right)$
33 32 rabbidv ${⊢}{a}={A}\to \left\{{l}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)|{a}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {l}\left({j}\right)\right)\left({k}\right)\right\}=\left\{{l}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)|{A}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {l}\left({j}\right)\right)\left({k}\right)\right\}$
34 ovexd ${⊢}{\phi }\to {ℝ}^{{X}}\in \mathrm{V}$
35 34 3 ssexd ${⊢}{\phi }\to {A}\in \mathrm{V}$
36 elpwg ${⊢}{A}\in \mathrm{V}\to \left({A}\in 𝒫\left({ℝ}^{{X}}\right)↔{A}\subseteq {ℝ}^{{X}}\right)$
37 35 36 syl ${⊢}{\phi }\to \left({A}\in 𝒫\left({ℝ}^{{X}}\right)↔{A}\subseteq {ℝ}^{{X}}\right)$
38 3 37 mpbird ${⊢}{\phi }\to {A}\in 𝒫\left({ℝ}^{{X}}\right)$
39 ovex ${⊢}{\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\in \mathrm{V}$
40 39 rabex ${⊢}\left\{{l}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)|{A}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {l}\left({j}\right)\right)\left({k}\right)\right\}\in \mathrm{V}$
41 40 a1i ${⊢}{\phi }\to \left\{{l}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)|{A}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {l}\left({j}\right)\right)\left({k}\right)\right\}\in \mathrm{V}$
42 5 33 38 41 fvmptd3 ${⊢}{\phi }\to {C}\left({A}\right)=\left\{{l}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)|{A}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {l}\left({j}\right)\right)\left({k}\right)\right\}$
43 42 eqcomd ${⊢}{\phi }\to \left\{{l}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)|{A}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {l}\left({j}\right)\right)\left({k}\right)\right\}={C}\left({A}\right)$
44 43 3ad2ant1 ${⊢}\left({\phi }\wedge {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\wedge {A}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)\to \left\{{l}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)|{A}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {l}\left({j}\right)\right)\left({k}\right)\right\}={C}\left({A}\right)$
45 31 44 eleqtrd ${⊢}\left({\phi }\wedge {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\wedge {A}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)\to {i}\in {C}\left({A}\right)$
46 19 20 21 45 syl3anc ${⊢}\left(\left({\phi }\wedge {z}\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\wedge {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\wedge \left({A}\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)\to {i}\in {C}\left({A}\right)$
47 coeq2 ${⊢}{h}={i}\left({j}\right)\to \left[.\right)\circ {h}=\left[.\right)\circ {i}\left({j}\right)$
48 47 fveq1d ${⊢}{h}={i}\left({j}\right)\to \left(\left[.\right)\circ {h}\right)\left({k}\right)=\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)$
49 48 fveq2d ${⊢}{h}={i}\left({j}\right)\to vol\left(\left(\left[.\right)\circ {h}\right)\left({k}\right)\right)=vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)$
50 49 prodeq2ad ${⊢}{h}={i}\left({j}\right)\to \prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {h}\right)\left({k}\right)\right)=\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)$
51 elmapi ${⊢}{i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\to {i}:ℕ⟶{{ℝ}^{2}}^{{X}}$
52 51 adantr ${⊢}\left({i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\wedge {j}\in ℕ\right)\to {i}:ℕ⟶{{ℝ}^{2}}^{{X}}$
53 simpr ${⊢}\left({i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\wedge {j}\in ℕ\right)\to {j}\in ℕ$
54 52 53 ffvelrnd ${⊢}\left({i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\wedge {j}\in ℕ\right)\to {i}\left({j}\right)\in \left({{ℝ}^{2}}^{{X}}\right)$
55 prodex ${⊢}\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)\in \mathrm{V}$
56 55 a1i ${⊢}\left({i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\wedge {j}\in ℕ\right)\to \prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)\in \mathrm{V}$
57 6 50 54 56 fvmptd3 ${⊢}\left({i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\wedge {j}\in ℕ\right)\to {L}\left({i}\left({j}\right)\right)=\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)$
58 57 mpteq2dva ${⊢}{i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\to \left({j}\in ℕ⟼{L}\left({i}\left({j}\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)$
59 58 fveq2d ${⊢}{i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\to \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\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)$
60 59 adantr ${⊢}\left({i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\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)\to \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\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)$
61 id ${⊢}{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)\to {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)$
62 61 eqcomd ${⊢}{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)\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)={z}$
63 62 adantl ${⊢}\left({i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\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)\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)={z}$
64 60 63 eqtrd ${⊢}\left({i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\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)\to \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)={z}$
65 64 3adant1 ${⊢}\left({z}\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\wedge {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\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)\to \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)={z}$
66 simp1 ${⊢}\left({z}\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\wedge {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\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)\to {z}\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}$
67 65 66 eqbrtrd ${⊢}\left({z}\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\wedge {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\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)\to \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}$
68 67 3adant1l ${⊢}\left(\left({\phi }\wedge {z}\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\wedge {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\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)\to \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}$
69 68 3adant3l ${⊢}\left(\left({\phi }\wedge {z}\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\wedge {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\wedge \left({A}\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)\to \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}$
70 46 69 jca ${⊢}\left(\left({\phi }\wedge {z}\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\wedge {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\wedge \left({A}\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)\to \left({i}\in {C}\left({A}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)$
71 70 19.8ad ${⊢}\left(\left({\phi }\wedge {z}\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\wedge {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\wedge \left({A}\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)\to \exists {i}\phantom{\rule{.4em}{0ex}}\left({i}\in {C}\left({A}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)$
72 71 3exp ${⊢}\left({\phi }\wedge {z}\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\to \left({i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\to \left(\left({A}\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)\to \exists {i}\phantom{\rule{.4em}{0ex}}\left({i}\in {C}\left({A}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\right)\right)$
73 17 18 72 rexlimd ${⊢}\left({\phi }\wedge {z}\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\to \left(\exists {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\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)\to \exists {i}\phantom{\rule{.4em}{0ex}}\left({i}\in {C}\left({A}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\right)$
74 73 imp ${⊢}\left(\left({\phi }\wedge {z}\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\wedge \exists {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\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)\to \exists {i}\phantom{\rule{.4em}{0ex}}\left({i}\in {C}\left({A}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)$
75 10 11 16 74 syl21anc ${⊢}\left({\phi }\wedge {z}\in \left\{{z}\in {ℝ}^{*}|\exists {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\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\}\wedge {z}\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\to \exists {i}\phantom{\rule{.4em}{0ex}}\left({i}\in {C}\left({A}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)$
76 75 3exp ${⊢}{\phi }\to \left({z}\in \left\{{z}\in {ℝ}^{*}|\exists {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\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\}\to \left({z}\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\to \exists {i}\phantom{\rule{.4em}{0ex}}\left({i}\in {C}\left({A}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\right)\right)$
77 76 rexlimdv ${⊢}{\phi }\to \left(\exists {z}\in \left\{{z}\in {ℝ}^{*}|\exists {i}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\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\}\phantom{\rule{.4em}{0ex}}{z}\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\to \exists {i}\phantom{\rule{.4em}{0ex}}\left({i}\in {C}\left({A}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\right)$
78 9 77 mpd ${⊢}{\phi }\to \exists {i}\phantom{\rule{.4em}{0ex}}\left({i}\in {C}\left({A}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)$
79 rabid ${⊢}{i}\in \left\{{i}\in {C}\left({A}\right)|\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right\}↔\left({i}\in {C}\left({A}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)$
80 79 bicomi ${⊢}\left({i}\in {C}\left({A}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)↔{i}\in \left\{{i}\in {C}\left({A}\right)|\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right\}$
81 80 biimpi ${⊢}\left({i}\in {C}\left({A}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\to {i}\in \left\{{i}\in {C}\left({A}\right)|\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right\}$
82 81 adantl ${⊢}\left({\phi }\wedge \left({i}\in {C}\left({A}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\right)\to {i}\in \left\{{i}\in {C}\left({A}\right)|\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right\}$
83 nfcv ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}\left({e}\in {ℝ}^{+}⟼\left\{{i}\in {C}\left({a}\right)|\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({a}\right){+}_{𝑒}{e}\right\}\right)$
84 nfcv ${⊢}\underset{_}{Ⅎ}{a}\phantom{\rule{.4em}{0ex}}{ℝ}^{+}$
85 nfv ${⊢}Ⅎ{a}\phantom{\rule{.4em}{0ex}}\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({b}\right){+}_{𝑒}{e}$
86 nfmpt1 ${⊢}\underset{_}{Ⅎ}{a}\phantom{\rule{.4em}{0ex}}\left({a}\in 𝒫\left({ℝ}^{{X}}\right)⟼\left\{{l}\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)|{a}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {l}\left({j}\right)\right)\left({k}\right)\right\}\right)$
87 5 86 nfcxfr ${⊢}\underset{_}{Ⅎ}{a}\phantom{\rule{.4em}{0ex}}{C}$
88 nfcv ${⊢}\underset{_}{Ⅎ}{a}\phantom{\rule{.4em}{0ex}}{b}$
89 87 88 nffv ${⊢}\underset{_}{Ⅎ}{a}\phantom{\rule{.4em}{0ex}}{C}\left({b}\right)$
90 85 89 nfrabw ${⊢}\underset{_}{Ⅎ}{a}\phantom{\rule{.4em}{0ex}}\left\{{i}\in {C}\left({b}\right)|\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({b}\right){+}_{𝑒}{e}\right\}$
91 84 90 nfmpt ${⊢}\underset{_}{Ⅎ}{a}\phantom{\rule{.4em}{0ex}}\left({e}\in {ℝ}^{+}⟼\left\{{i}\in {C}\left({b}\right)|\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({b}\right){+}_{𝑒}{e}\right\}\right)$
92 fveq2 ${⊢}{a}={b}\to {C}\left({a}\right)={C}\left({b}\right)$
93 92 eleq2d ${⊢}{a}={b}\to \left({i}\in {C}\left({a}\right)↔{i}\in {C}\left({b}\right)\right)$
94 fveq2 ${⊢}{a}={b}\to \mathrm{voln*}\left({X}\right)\left({a}\right)=\mathrm{voln*}\left({X}\right)\left({b}\right)$
95 94 oveq1d ${⊢}{a}={b}\to \mathrm{voln*}\left({X}\right)\left({a}\right){+}_{𝑒}{e}=\mathrm{voln*}\left({X}\right)\left({b}\right){+}_{𝑒}{e}$
96 95 breq2d ${⊢}{a}={b}\to \left(\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({a}\right){+}_{𝑒}{e}↔\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({b}\right){+}_{𝑒}{e}\right)$
97 93 96 anbi12d ${⊢}{a}={b}\to \left(\left({i}\in {C}\left({a}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({a}\right){+}_{𝑒}{e}\right)↔\left({i}\in {C}\left({b}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({b}\right){+}_{𝑒}{e}\right)\right)$
98 97 rabbidva2 ${⊢}{a}={b}\to \left\{{i}\in {C}\left({a}\right)|\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({a}\right){+}_{𝑒}{e}\right\}=\left\{{i}\in {C}\left({b}\right)|\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({b}\right){+}_{𝑒}{e}\right\}$
99 98 mpteq2dv ${⊢}{a}={b}\to \left({e}\in {ℝ}^{+}⟼\left\{{i}\in {C}\left({a}\right)|\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({a}\right){+}_{𝑒}{e}\right\}\right)=\left({e}\in {ℝ}^{+}⟼\left\{{i}\in {C}\left({b}\right)|\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({b}\right){+}_{𝑒}{e}\right\}\right)$
100 83 91 99 cbvmpt ${⊢}\left({a}\in 𝒫\left({ℝ}^{{X}}\right)⟼\left({e}\in {ℝ}^{+}⟼\left\{{i}\in {C}\left({a}\right)|\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({a}\right){+}_{𝑒}{e}\right\}\right)\right)=\left({b}\in 𝒫\left({ℝ}^{{X}}\right)⟼\left({e}\in {ℝ}^{+}⟼\left\{{i}\in {C}\left({b}\right)|\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({b}\right){+}_{𝑒}{e}\right\}\right)\right)$
101 7 100 eqtri ${⊢}{D}=\left({b}\in 𝒫\left({ℝ}^{{X}}\right)⟼\left({e}\in {ℝ}^{+}⟼\left\{{i}\in {C}\left({b}\right)|\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({b}\right){+}_{𝑒}{e}\right\}\right)\right)$
102 fveq2 ${⊢}{b}={A}\to {C}\left({b}\right)={C}\left({A}\right)$
103 102 eleq2d ${⊢}{b}={A}\to \left({i}\in {C}\left({b}\right)↔{i}\in {C}\left({A}\right)\right)$
104 fveq2 ${⊢}{b}={A}\to \mathrm{voln*}\left({X}\right)\left({b}\right)=\mathrm{voln*}\left({X}\right)\left({A}\right)$
105 104 oveq1d ${⊢}{b}={A}\to \mathrm{voln*}\left({X}\right)\left({b}\right){+}_{𝑒}{e}=\mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{e}$
106 105 breq2d ${⊢}{b}={A}\to \left(\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({b}\right){+}_{𝑒}{e}↔\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{e}\right)$
107 103 106 anbi12d ${⊢}{b}={A}\to \left(\left({i}\in {C}\left({b}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({b}\right){+}_{𝑒}{e}\right)↔\left({i}\in {C}\left({A}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{e}\right)\right)$
108 107 rabbidva2 ${⊢}{b}={A}\to \left\{{i}\in {C}\left({b}\right)|\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({b}\right){+}_{𝑒}{e}\right\}=\left\{{i}\in {C}\left({A}\right)|\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{e}\right\}$
109 108 mpteq2dv ${⊢}{b}={A}\to \left({e}\in {ℝ}^{+}⟼\left\{{i}\in {C}\left({b}\right)|\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({b}\right){+}_{𝑒}{e}\right\}\right)=\left({e}\in {ℝ}^{+}⟼\left\{{i}\in {C}\left({A}\right)|\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{e}\right\}\right)$
110 38 adantr ${⊢}\left({\phi }\wedge \left({i}\in {C}\left({A}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\right)\to {A}\in 𝒫\left({ℝ}^{{X}}\right)$
111 rpex ${⊢}{ℝ}^{+}\in \mathrm{V}$
112 111 mptex ${⊢}\left({e}\in {ℝ}^{+}⟼\left\{{i}\in {C}\left({A}\right)|\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{e}\right\}\right)\in \mathrm{V}$
113 112 a1i ${⊢}\left({\phi }\wedge \left({i}\in {C}\left({A}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\right)\to \left({e}\in {ℝ}^{+}⟼\left\{{i}\in {C}\left({A}\right)|\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{e}\right\}\right)\in \mathrm{V}$
114 101 109 110 113 fvmptd3 ${⊢}\left({\phi }\wedge \left({i}\in {C}\left({A}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\right)\to {D}\left({A}\right)=\left({e}\in {ℝ}^{+}⟼\left\{{i}\in {C}\left({A}\right)|\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{e}\right\}\right)$
115 oveq2 ${⊢}{e}={E}\to \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{e}=\mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}$
116 115 breq2d ${⊢}{e}={E}\to \left(\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{e}↔\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)$
117 116 rabbidv ${⊢}{e}={E}\to \left\{{i}\in {C}\left({A}\right)|\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{e}\right\}=\left\{{i}\in {C}\left({A}\right)|\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right\}$
118 117 adantl ${⊢}\left(\left({\phi }\wedge \left({i}\in {C}\left({A}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\right)\wedge {e}={E}\right)\to \left\{{i}\in {C}\left({A}\right)|\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{e}\right\}=\left\{{i}\in {C}\left({A}\right)|\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right\}$
119 4 adantr ${⊢}\left({\phi }\wedge \left({i}\in {C}\left({A}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\right)\to {E}\in {ℝ}^{+}$
120 fvex ${⊢}{C}\left({A}\right)\in \mathrm{V}$
121 120 rabex ${⊢}\left\{{i}\in {C}\left({A}\right)|\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right\}\in \mathrm{V}$
122 121 a1i ${⊢}\left({\phi }\wedge \left({i}\in {C}\left({A}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\right)\to \left\{{i}\in {C}\left({A}\right)|\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right\}\in \mathrm{V}$
123 114 118 119 122 fvmptd ${⊢}\left({\phi }\wedge \left({i}\in {C}\left({A}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\right)\to {D}\left({A}\right)\left({E}\right)=\left\{{i}\in {C}\left({A}\right)|\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right\}$
124 123 eqcomd ${⊢}\left({\phi }\wedge \left({i}\in {C}\left({A}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\right)\to \left\{{i}\in {C}\left({A}\right)|\mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right\}={D}\left({A}\right)\left({E}\right)$
125 82 124 eleqtrd ${⊢}\left({\phi }\wedge \left({i}\in {C}\left({A}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\right)\to {i}\in {D}\left({A}\right)\left({E}\right)$
126 125 ex ${⊢}{\phi }\to \left(\left({i}\in {C}\left({A}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\to {i}\in {D}\left({A}\right)\left({E}\right)\right)$
127 126 eximdv ${⊢}{\phi }\to \left(\exists {i}\phantom{\rule{.4em}{0ex}}\left({i}\in {C}\left({A}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{L}\left({i}\left({j}\right)\right)\right)\right)\le \mathrm{voln*}\left({X}\right)\left({A}\right){+}_{𝑒}{E}\right)\to \exists {i}\phantom{\rule{.4em}{0ex}}{i}\in {D}\left({A}\right)\left({E}\right)\right)$
128 78 127 mpd ${⊢}{\phi }\to \exists {i}\phantom{\rule{.4em}{0ex}}{i}\in {D}\left({A}\right)\left({E}\right)$