# Metamath Proof Explorer

## Theorem ovnlecvr2

Description: Given a subset of multidimensional reals and a set of half-open intervals that covers it, the Lebesgue outer measure of the set is bounded by the generalized sum of the pre-measure of the half-open intervals. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses ovnlecvr2.x ${⊢}{\phi }\to {X}\in \mathrm{Fin}$
ovnlecvr2.c ${⊢}{\phi }\to {C}:ℕ⟶{ℝ}^{{X}}$
ovnlecvr2.d ${⊢}{\phi }\to {D}:ℕ⟶{ℝ}^{{X}}$
ovnlecvr2.s ${⊢}{\phi }\to {A}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)$
ovnlecvr2.l ${⊢}{L}=\left({x}\in \mathrm{Fin}⟼\left({a}\in \left({ℝ}^{{x}}\right),{b}\in \left({ℝ}^{{x}}\right)⟼if\left({x}=\varnothing ,0,\prod _{{k}\in {x}}vol\left(\left[{a}\left({k}\right),{b}\left({k}\right)\right)\right)\right)\right)\right)$
Assertion ovnlecvr2 ${⊢}{\phi }\to \mathrm{voln*}\left({X}\right)\left({A}\right)\le \mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 ovnlecvr2.x ${⊢}{\phi }\to {X}\in \mathrm{Fin}$
2 ovnlecvr2.c ${⊢}{\phi }\to {C}:ℕ⟶{ℝ}^{{X}}$
3 ovnlecvr2.d ${⊢}{\phi }\to {D}:ℕ⟶{ℝ}^{{X}}$
4 ovnlecvr2.s ${⊢}{\phi }\to {A}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)$
5 ovnlecvr2.l ${⊢}{L}=\left({x}\in \mathrm{Fin}⟼\left({a}\in \left({ℝ}^{{x}}\right),{b}\in \left({ℝ}^{{x}}\right)⟼if\left({x}=\varnothing ,0,\prod _{{k}\in {x}}vol\left(\left[{a}\left({k}\right),{b}\left({k}\right)\right)\right)\right)\right)\right)$
6 fveq2 ${⊢}{X}=\varnothing \to \mathrm{voln*}\left({X}\right)=\mathrm{voln*}\left(\varnothing \right)$
7 6 fveq1d ${⊢}{X}=\varnothing \to \mathrm{voln*}\left({X}\right)\left({A}\right)=\mathrm{voln*}\left(\varnothing \right)\left({A}\right)$
8 7 adantl ${⊢}\left({\phi }\wedge {X}=\varnothing \right)\to \mathrm{voln*}\left({X}\right)\left({A}\right)=\mathrm{voln*}\left(\varnothing \right)\left({A}\right)$
9 4 adantr ${⊢}\left({\phi }\wedge {X}=\varnothing \right)\to {A}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)$
10 1nn ${⊢}1\in ℕ$
11 ne0i ${⊢}1\in ℕ\to ℕ\ne \varnothing$
12 10 11 ax-mp ${⊢}ℕ\ne \varnothing$
13 12 a1i ${⊢}{\phi }\to ℕ\ne \varnothing$
14 iunconst ${⊢}ℕ\ne \varnothing \to \bigcup _{{j}\in ℕ}\left\{\varnothing \right\}=\left\{\varnothing \right\}$
15 13 14 syl ${⊢}{\phi }\to \bigcup _{{j}\in ℕ}\left\{\varnothing \right\}=\left\{\varnothing \right\}$
16 15 adantr ${⊢}\left({\phi }\wedge {X}=\varnothing \right)\to \bigcup _{{j}\in ℕ}\left\{\varnothing \right\}=\left\{\varnothing \right\}$
17 ixpeq1 ${⊢}{X}=\varnothing \to \underset{{k}\in {X}}{⨉}\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)=\underset{{k}\in \varnothing }{⨉}\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)$
18 ixp0x ${⊢}\underset{{k}\in \varnothing }{⨉}\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)=\left\{\varnothing \right\}$
19 18 a1i ${⊢}{X}=\varnothing \to \underset{{k}\in \varnothing }{⨉}\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)=\left\{\varnothing \right\}$
20 17 19 eqtrd ${⊢}{X}=\varnothing \to \underset{{k}\in {X}}{⨉}\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)=\left\{\varnothing \right\}$
21 20 adantr ${⊢}\left({X}=\varnothing \wedge {j}\in ℕ\right)\to \underset{{k}\in {X}}{⨉}\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)=\left\{\varnothing \right\}$
22 21 iuneq2dv ${⊢}{X}=\varnothing \to \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)=\bigcup _{{j}\in ℕ}\left\{\varnothing \right\}$
23 22 adantl ${⊢}\left({\phi }\wedge {X}=\varnothing \right)\to \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)=\bigcup _{{j}\in ℕ}\left\{\varnothing \right\}$
24 reex ${⊢}ℝ\in \mathrm{V}$
25 mapdm0 ${⊢}ℝ\in \mathrm{V}\to {ℝ}^{\varnothing }=\left\{\varnothing \right\}$
26 24 25 ax-mp ${⊢}{ℝ}^{\varnothing }=\left\{\varnothing \right\}$
27 26 a1i ${⊢}\left({\phi }\wedge {X}=\varnothing \right)\to {ℝ}^{\varnothing }=\left\{\varnothing \right\}$
28 16 23 27 3eqtr4d ${⊢}\left({\phi }\wedge {X}=\varnothing \right)\to \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)={ℝ}^{\varnothing }$
29 9 28 sseqtrd ${⊢}\left({\phi }\wedge {X}=\varnothing \right)\to {A}\subseteq {ℝ}^{\varnothing }$
30 29 ovn0val ${⊢}\left({\phi }\wedge {X}=\varnothing \right)\to \mathrm{voln*}\left(\varnothing \right)\left({A}\right)=0$
31 8 30 eqtrd ${⊢}\left({\phi }\wedge {X}=\varnothing \right)\to \mathrm{voln*}\left({X}\right)\left({A}\right)=0$
32 nfv ${⊢}Ⅎ{j}\phantom{\rule{.4em}{0ex}}{\phi }$
33 nnex ${⊢}ℕ\in \mathrm{V}$
34 33 a1i ${⊢}{\phi }\to ℕ\in \mathrm{V}$
35 icossicc ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq \left[0,\mathrm{+\infty }\right]$
36 1 adantr ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to {X}\in \mathrm{Fin}$
37 2 ffvelrnda ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to {C}\left({j}\right)\in \left({ℝ}^{{X}}\right)$
38 elmapi ${⊢}{C}\left({j}\right)\in \left({ℝ}^{{X}}\right)\to {C}\left({j}\right):{X}⟶ℝ$
39 37 38 syl ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to {C}\left({j}\right):{X}⟶ℝ$
40 3 ffvelrnda ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to {D}\left({j}\right)\in \left({ℝ}^{{X}}\right)$
41 elmapi ${⊢}{D}\left({j}\right)\in \left({ℝ}^{{X}}\right)\to {D}\left({j}\right):{X}⟶ℝ$
42 40 41 syl ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to {D}\left({j}\right):{X}⟶ℝ$
43 5 36 39 42 hoidmvcl ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to {C}\left({j}\right){L}\left({X}\right){D}\left({j}\right)\in \left[0,\mathrm{+\infty }\right)$
44 35 43 sseldi ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to {C}\left({j}\right){L}\left({X}\right){D}\left({j}\right)\in \left[0,\mathrm{+\infty }\right]$
45 32 34 44 sge0ge0mpt ${⊢}{\phi }\to 0\le \mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\right)\right)\right)$
46 45 adantr ${⊢}\left({\phi }\wedge {X}=\varnothing \right)\to 0\le \mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\right)\right)\right)$
47 31 46 eqbrtrd ${⊢}\left({\phi }\wedge {X}=\varnothing \right)\to \mathrm{voln*}\left({X}\right)\left({A}\right)\le \mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\right)\right)\right)$
48 simpl ${⊢}\left({\phi }\wedge ¬{X}=\varnothing \right)\to {\phi }$
49 neqne ${⊢}¬{X}=\varnothing \to {X}\ne \varnothing$
50 49 adantl ${⊢}\left({\phi }\wedge ¬{X}=\varnothing \right)\to {X}\ne \varnothing$
51 1 adantr ${⊢}\left({\phi }\wedge {X}\ne \varnothing \right)\to {X}\in \mathrm{Fin}$
52 simpr ${⊢}\left({\phi }\wedge {X}\ne \varnothing \right)\to {X}\ne \varnothing$
53 39 ffvelrnda ${⊢}\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge {k}\in {X}\right)\to {C}\left({j}\right)\left({k}\right)\in ℝ$
54 42 ffvelrnda ${⊢}\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge {k}\in {X}\right)\to {D}\left({j}\right)\left({k}\right)\in ℝ$
55 54 rexrd ${⊢}\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge {k}\in {X}\right)\to {D}\left({j}\right)\left({k}\right)\in {ℝ}^{*}$
56 icossre ${⊢}\left({C}\left({j}\right)\left({k}\right)\in ℝ\wedge {D}\left({j}\right)\left({k}\right)\in {ℝ}^{*}\right)\to \left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)\subseteq ℝ$
57 53 55 56 syl2anc ${⊢}\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge {k}\in {X}\right)\to \left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)\subseteq ℝ$
58 57 ralrimiva ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to \forall {k}\in {X}\phantom{\rule{.4em}{0ex}}\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)\subseteq ℝ$
59 ss2ixp ${⊢}\forall {k}\in {X}\phantom{\rule{.4em}{0ex}}\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)\subseteq ℝ\to \underset{{k}\in {X}}{⨉}\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)\subseteq \underset{{k}\in {X}}{⨉}ℝ$
60 58 59 syl ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to \underset{{k}\in {X}}{⨉}\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)\subseteq \underset{{k}\in {X}}{⨉}ℝ$
61 24 a1i ${⊢}{\phi }\to ℝ\in \mathrm{V}$
62 ixpconstg ${⊢}\left({X}\in \mathrm{Fin}\wedge ℝ\in \mathrm{V}\right)\to \underset{{k}\in {X}}{⨉}ℝ={ℝ}^{{X}}$
63 1 61 62 syl2anc ${⊢}{\phi }\to \underset{{k}\in {X}}{⨉}ℝ={ℝ}^{{X}}$
64 63 adantr ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to \underset{{k}\in {X}}{⨉}ℝ={ℝ}^{{X}}$
65 60 64 sseqtrd ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to \underset{{k}\in {X}}{⨉}\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)\subseteq {ℝ}^{{X}}$
66 65 ralrimiva ${⊢}{\phi }\to \forall {j}\in ℕ\phantom{\rule{.4em}{0ex}}\underset{{k}\in {X}}{⨉}\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)\subseteq {ℝ}^{{X}}$
67 iunss ${⊢}\bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)\subseteq {ℝ}^{{X}}↔\forall {j}\in ℕ\phantom{\rule{.4em}{0ex}}\underset{{k}\in {X}}{⨉}\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)\subseteq {ℝ}^{{X}}$
68 66 67 sylibr ${⊢}{\phi }\to \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)\subseteq {ℝ}^{{X}}$
69 4 68 sstrd ${⊢}{\phi }\to {A}\subseteq {ℝ}^{{X}}$
70 69 adantr ${⊢}\left({\phi }\wedge {X}\ne \varnothing \right)\to {A}\subseteq {ℝ}^{{X}}$
71 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\}$
72 51 52 70 71 ovnn0val ${⊢}\left({\phi }\wedge {X}\ne \varnothing \right)\to \mathrm{voln*}\left({X}\right)\left({A}\right)=sup\left(\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\},{ℝ}^{*},<\right)$
73 ssrab2 ${⊢}\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\}\subseteq {ℝ}^{*}$
74 73 a1i ${⊢}\left({\phi }\wedge {X}\ne \varnothing \right)\to \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\}\subseteq {ℝ}^{*}$
75 32 34 44 sge0xrclmpt ${⊢}{\phi }\to \mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\right)\right)\right)\in {ℝ}^{*}$
76 75 adantr ${⊢}\left({\phi }\wedge {X}\ne \varnothing \right)\to \mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\right)\right)\right)\in {ℝ}^{*}$
77 opelxpi ${⊢}\left({C}\left({j}\right)\left({k}\right)\in ℝ\wedge {D}\left({j}\right)\left({k}\right)\in ℝ\right)\to ⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\in {ℝ}^{2}$
78 53 54 77 syl2anc ${⊢}\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge {k}\in {X}\right)\to ⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\in {ℝ}^{2}$
79 78 fmpttd ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to \left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right):{X}⟶{ℝ}^{2}$
80 24 24 xpex ${⊢}{ℝ}^{2}\in \mathrm{V}$
81 80 a1i ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to {ℝ}^{2}\in \mathrm{V}$
82 elmapg ${⊢}\left({ℝ}^{2}\in \mathrm{V}\wedge {X}\in \mathrm{Fin}\right)\to \left(\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\in \left({{ℝ}^{2}}^{{X}}\right)↔\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right):{X}⟶{ℝ}^{2}\right)$
83 81 36 82 syl2anc ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to \left(\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\in \left({{ℝ}^{2}}^{{X}}\right)↔\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right):{X}⟶{ℝ}^{2}\right)$
84 79 83 mpbird ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to \left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\in \left({{ℝ}^{2}}^{{X}}\right)$
85 84 fmpttd ${⊢}{\phi }\to \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right):ℕ⟶{{ℝ}^{2}}^{{X}}$
86 ovexd ${⊢}{\phi }\to {{ℝ}^{2}}^{{X}}\in \mathrm{V}$
87 elmapg ${⊢}\left({{ℝ}^{2}}^{{X}}\in \mathrm{V}\wedge ℕ\in \mathrm{V}\right)\to \left(\left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)↔\left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right):ℕ⟶{{ℝ}^{2}}^{{X}}\right)$
88 86 34 87 syl2anc ${⊢}{\phi }\to \left(\left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)↔\left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right):ℕ⟶{{ℝ}^{2}}^{{X}}\right)$
89 85 88 mpbird ${⊢}{\phi }\to \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)$
90 89 adantr ${⊢}\left({\phi }\wedge {X}\ne \varnothing \right)\to \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)$
91 simpr ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to {j}\in ℕ$
92 mptexg ${⊢}{X}\in \mathrm{Fin}\to \left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\in \mathrm{V}$
93 1 92 syl ${⊢}{\phi }\to \left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\in \mathrm{V}$
94 93 adantr ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to \left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\in \mathrm{V}$
95 eqid ${⊢}\left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)=\left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)$
96 95 fvmpt2 ${⊢}\left({j}\in ℕ\wedge \left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\in \mathrm{V}\right)\to \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)=\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)$
97 91 94 96 syl2anc ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)=\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)$
98 97 coeq2d ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to \left[.\right)\circ \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)=\left[.\right)\circ \left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)$
99 98 fveq1d ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to \left(\left[.\right)\circ \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)=\left(\left[.\right)\circ \left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({k}\right)$
100 99 adantr ${⊢}\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge {k}\in {X}\right)\to \left(\left[.\right)\circ \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)=\left(\left[.\right)\circ \left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({k}\right)$
101 79 adantr ${⊢}\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge {k}\in {X}\right)\to \left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right):{X}⟶{ℝ}^{2}$
102 simpr ${⊢}\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge {k}\in {X}\right)\to {k}\in {X}$
103 101 102 fvovco ${⊢}\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge {k}\in {X}\right)\to \left(\left[.\right)\circ \left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({k}\right)=\left[{1}^{st}\left(\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\left({k}\right)\right),{2}^{nd}\left(\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\left({k}\right)\right)\right)$
104 simpr ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to {k}\in {X}$
105 opex ${⊢}⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\in \mathrm{V}$
106 105 a1i ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to ⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\in \mathrm{V}$
107 eqid ${⊢}\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)=\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)$
108 107 fvmpt2 ${⊢}\left({k}\in {X}\wedge ⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\in \mathrm{V}\right)\to \left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\left({k}\right)=⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩$
109 104 106 108 syl2anc ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to \left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\left({k}\right)=⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩$
110 109 fveq2d ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to {1}^{st}\left(\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\left({k}\right)\right)={1}^{st}\left(⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)$
111 fvex ${⊢}{C}\left({j}\right)\left({k}\right)\in \mathrm{V}$
112 fvex ${⊢}{D}\left({j}\right)\left({k}\right)\in \mathrm{V}$
113 op1stg ${⊢}\left({C}\left({j}\right)\left({k}\right)\in \mathrm{V}\wedge {D}\left({j}\right)\left({k}\right)\in \mathrm{V}\right)\to {1}^{st}\left(⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)={C}\left({j}\right)\left({k}\right)$
114 111 112 113 mp2an ${⊢}{1}^{st}\left(⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)={C}\left({j}\right)\left({k}\right)$
115 114 a1i ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to {1}^{st}\left(⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)={C}\left({j}\right)\left({k}\right)$
116 110 115 eqtrd ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to {1}^{st}\left(\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\left({k}\right)\right)={C}\left({j}\right)\left({k}\right)$
117 109 fveq2d ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to {2}^{nd}\left(\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\left({k}\right)\right)={2}^{nd}\left(⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)$
118 111 112 op2nd ${⊢}{2}^{nd}\left(⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)={D}\left({j}\right)\left({k}\right)$
119 118 a1i ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to {2}^{nd}\left(⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)={D}\left({j}\right)\left({k}\right)$
120 117 119 eqtrd ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to {2}^{nd}\left(\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\left({k}\right)\right)={D}\left({j}\right)\left({k}\right)$
121 116 120 oveq12d ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to \left[{1}^{st}\left(\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\left({k}\right)\right),{2}^{nd}\left(\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\left({k}\right)\right)\right)=\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)$
122 121 adantlr ${⊢}\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge {k}\in {X}\right)\to \left[{1}^{st}\left(\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\left({k}\right)\right),{2}^{nd}\left(\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\left({k}\right)\right)\right)=\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)$
123 100 103 122 3eqtrrd ${⊢}\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge {k}\in {X}\right)\to \left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)=\left(\left[.\right)\circ \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)$
124 123 ixpeq2dva ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to \underset{{k}\in {X}}{⨉}\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)=\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)$
125 124 iuneq2dv ${⊢}{\phi }\to \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)=\bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)$
126 4 125 sseqtrd ${⊢}{\phi }\to {A}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)$
127 126 adantr ${⊢}\left({\phi }\wedge {X}\ne \varnothing \right)\to {A}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)$
128 eqidd ${⊢}\left({\phi }\wedge {X}\ne \varnothing \right)\to \mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {X}}vol\left(\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)\right)\right)\right)=\mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {X}}vol\left(\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)\right)\right)\right)$
129 51 adantr ${⊢}\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {j}\in ℕ\right)\to {X}\in \mathrm{Fin}$
130 52 adantr ${⊢}\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {j}\in ℕ\right)\to {X}\ne \varnothing$
131 39 adantlr ${⊢}\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {j}\in ℕ\right)\to {C}\left({j}\right):{X}⟶ℝ$
132 42 adantlr ${⊢}\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {j}\in ℕ\right)\to {D}\left({j}\right):{X}⟶ℝ$
133 5 129 130 131 132 hoidmvn0val ${⊢}\left(\left({\phi }\wedge {X}\ne \varnothing \right)\wedge {j}\in ℕ\right)\to {C}\left({j}\right){L}\left({X}\right){D}\left({j}\right)=\prod _{{k}\in {X}}vol\left(\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)\right)$
134 133 mpteq2dva ${⊢}\left({\phi }\wedge {X}\ne \varnothing \right)\to \left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\right)\right)=\left({j}\in ℕ⟼\prod _{{k}\in {X}}vol\left(\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)\right)\right)$
135 134 fveq2d ${⊢}\left({\phi }\wedge {X}\ne \varnothing \right)\to \mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\right)\right)\right)=\mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {X}}vol\left(\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)\right)\right)\right)$
136 123 eqcomd ${⊢}\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge {k}\in {X}\right)\to \left(\left[.\right)\circ \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)=\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)$
137 136 fveq2d ${⊢}\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge {k}\in {X}\right)\to vol\left(\left(\left[.\right)\circ \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)\right)=vol\left(\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)\right)$
138 137 prodeq2dv ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to \prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)\right)=\prod _{{k}\in {X}}vol\left(\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)\right)$
139 138 mpteq2dva ${⊢}{\phi }\to \left({j}\in ℕ⟼\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)\right)\right)=\left({j}\in ℕ⟼\prod _{{k}\in {X}}vol\left(\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)\right)\right)$
140 139 fveq2d ${⊢}{\phi }\to \mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)\right)\right)\right)=\mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {X}}vol\left(\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)\right)\right)\right)$
141 140 adantr ${⊢}\left({\phi }\wedge {X}\ne \varnothing \right)\to \mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)\right)\right)\right)=\mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {X}}vol\left(\left[{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)\right)\right)\right)\right)$
142 128 135 141 3eqtr4d ${⊢}\left({\phi }\wedge {X}\ne \varnothing \right)\to \mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\right)\right)\right)=\mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)\right)\right)\right)$
143 127 142 jca ${⊢}\left({\phi }\wedge {X}\ne \varnothing \right)\to \left({A}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\right)\right)\right)=\mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)\right)\right)\right)\right)$
144 nfcv ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}{i}$
145 nfmpt1 ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}\left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)$
146 144 145 nfeq ${⊢}Ⅎ{j}\phantom{\rule{.4em}{0ex}}{i}=\left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)$
147 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{i}$
148 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}ℕ$
149 nfmpt1 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)$
150 148 149 nfmpt ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)$
151 147 150 nfeq ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{i}=\left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)$
152 fveq1 ${⊢}{i}=\left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\to {i}\left({j}\right)=\left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)$
153 152 coeq2d ${⊢}{i}=\left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\to \left[.\right)\circ {i}\left({j}\right)=\left[.\right)\circ \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)$
154 153 fveq1d ${⊢}{i}=\left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\to \left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)=\left(\left[.\right)\circ \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)$
155 154 adantr ${⊢}\left({i}=\left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\wedge {k}\in {X}\right)\to \left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)=\left(\left[.\right)\circ \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)$
156 151 155 ixpeq2d ${⊢}{i}=\left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\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 \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)$
157 156 adantr ${⊢}\left({i}=\left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\wedge {j}\in ℕ\right)\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 \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)$
158 146 157 iuneq2df ${⊢}{i}=\left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\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 \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)$
159 158 sseq2d ${⊢}{i}=\left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\to \left({A}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)↔{A}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)\right)$
160 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{j}\in ℕ$
161 151 160 nfan ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left({i}=\left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\wedge {j}\in ℕ\right)$
162 154 fveq2d ${⊢}{i}=\left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\to vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)=vol\left(\left(\left[.\right)\circ \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)\right)$
163 162 a1d ${⊢}{i}=\left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\to \left({k}\in {X}\to vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)=vol\left(\left(\left[.\right)\circ \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)\right)\right)$
164 163 adantr ${⊢}\left({i}=\left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\wedge {j}\in ℕ\right)\to \left({k}\in {X}\to vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)=vol\left(\left(\left[.\right)\circ \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)\right)\right)$
165 161 164 ralrimi ${⊢}\left({i}=\left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\wedge {j}\in ℕ\right)\to \forall {k}\in {X}\phantom{\rule{.4em}{0ex}}vol\left(\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\right)=vol\left(\left(\left[.\right)\circ \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)\right)$
166 165 prodeq2d ${⊢}\left({i}=\left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\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)=\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)\right)$
167 146 166 mpteq2da ${⊢}{i}=\left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\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 \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)\right)\right)$
168 167 fveq2d ${⊢}{i}=\left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\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)=\mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)\right)\right)\right)$
169 168 eqeq2d ${⊢}{i}=\left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\to \left(\mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\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)↔\mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\right)\right)\right)=\mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)\right)\right)\right)\right)$
170 159 169 anbi12d ${⊢}{i}=\left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\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 \mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\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)\right)↔\left({A}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\right)\right)\right)=\mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)\right)\right)\right)\right)\right)$
171 170 rspcev ${⊢}\left(\left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\in \left({\left({{ℝ}^{2}}^{{X}}\right)}^{ℕ}\right)\wedge \left({A}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\left({j}\right)\right)\left({k}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\right)\right)\right)=\mathrm{sum^}\left(\left({j}\in ℕ⟼\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ \left({j}\in ℕ⟼\left({k}\in {X}⟼⟨{C}\left({j}\right)\left({k}\right),{D}\left({j}\right)\left({k}\right)⟩\right)\right)\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 \mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\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)\right)$
172 90 143 171 syl2anc ${⊢}\left({\phi }\wedge {X}\ne \varnothing \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 \mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\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)\right)$
173 76 172 jca ${⊢}\left({\phi }\wedge {X}\ne \varnothing \right)\to \left(\mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\right)\right)\right)\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 \mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\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)\right)\right)$
174 eqeq1 ${⊢}{z}=\mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\right)\right)\right)\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)↔\mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\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)\right)$
175 174 anbi2d ${⊢}{z}=\mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\right)\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)↔\left({A}\subseteq \bigcup _{{j}\in ℕ}\underset{{k}\in {X}}{⨉}\left(\left[.\right)\circ {i}\left({j}\right)\right)\left({k}\right)\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\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)\right)\right)$
176 175 rexbidv ${⊢}{z}=\mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\right)\right)\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)↔\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 \mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\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)\right)\right)$
177 176 elrab ${⊢}\mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\right)\right)\right)\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(\mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\right)\right)\right)\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 \mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\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)\right)\right)$
178 173 177 sylibr ${⊢}\left({\phi }\wedge {X}\ne \varnothing \right)\to \mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\right)\right)\right)\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\}$
179 infxrlb ${⊢}\left(\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\}\subseteq {ℝ}^{*}\wedge \mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\right)\right)\right)\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\}\right)\to sup\left(\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\},{ℝ}^{*},<\right)\le \mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\right)\right)\right)$
180 74 178 179 syl2anc ${⊢}\left({\phi }\wedge {X}\ne \varnothing \right)\to sup\left(\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\},{ℝ}^{*},<\right)\le \mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\right)\right)\right)$
181 72 180 eqbrtrd ${⊢}\left({\phi }\wedge {X}\ne \varnothing \right)\to \mathrm{voln*}\left({X}\right)\left({A}\right)\le \mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\right)\right)\right)$
182 48 50 181 syl2anc ${⊢}\left({\phi }\wedge ¬{X}=\varnothing \right)\to \mathrm{voln*}\left({X}\right)\left({A}\right)\le \mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\right)\right)\right)$
183 47 182 pm2.61dan ${⊢}{\phi }\to \mathrm{voln*}\left({X}\right)\left({A}\right)\le \mathrm{sum^}\left(\left({j}\in ℕ⟼{C}\left({j}\right){L}\left({X}\right){D}\left({j}\right)\right)\right)$