# Metamath Proof Explorer

## Theorem ovoliunlem2

Description: Lemma for ovoliun . (Contributed by Mario Carneiro, 12-Jun-2014)

Ref Expression
Hypotheses ovoliun.t ${⊢}{T}=seq1\left(+,{G}\right)$
ovoliun.g ${⊢}{G}=\left({n}\in ℕ⟼{vol}^{*}\left({A}\right)\right)$
ovoliun.a ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {A}\subseteq ℝ$
ovoliun.v ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {vol}^{*}\left({A}\right)\in ℝ$
ovoliun.r ${⊢}{\phi }\to sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\in ℝ$
ovoliun.b ${⊢}{\phi }\to {B}\in {ℝ}^{+}$
ovoliun.s ${⊢}{S}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\left({n}\right)\right)\right)$
ovoliun.u ${⊢}{U}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {H}\right)\right)$
ovoliun.h ${⊢}{H}=\left({k}\in ℕ⟼{F}\left({1}^{st}\left({J}\left({k}\right)\right)\right)\left({2}^{nd}\left({J}\left({k}\right)\right)\right)\right)$
ovoliun.j ${⊢}{\phi }\to {J}:ℕ\underset{1-1 onto}{⟶}ℕ×ℕ$
ovoliun.f ${⊢}{\phi }\to {F}:ℕ⟶{\left(\le \cap {ℝ}^{2}\right)}^{ℕ}$
ovoliun.x1 ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\left({n}\right)\right)$
ovoliun.x2 ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+\left(\frac{{B}}{{2}^{{n}}}\right)$
Assertion ovoliunlem2 ${⊢}{\phi }\to {vol}^{*}\left(\bigcup _{{n}\in ℕ}{A}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{B}$

### Proof

Step Hyp Ref Expression
1 ovoliun.t ${⊢}{T}=seq1\left(+,{G}\right)$
2 ovoliun.g ${⊢}{G}=\left({n}\in ℕ⟼{vol}^{*}\left({A}\right)\right)$
3 ovoliun.a ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {A}\subseteq ℝ$
4 ovoliun.v ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {vol}^{*}\left({A}\right)\in ℝ$
5 ovoliun.r ${⊢}{\phi }\to sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\in ℝ$
6 ovoliun.b ${⊢}{\phi }\to {B}\in {ℝ}^{+}$
7 ovoliun.s ${⊢}{S}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\left({n}\right)\right)\right)$
8 ovoliun.u ${⊢}{U}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {H}\right)\right)$
9 ovoliun.h ${⊢}{H}=\left({k}\in ℕ⟼{F}\left({1}^{st}\left({J}\left({k}\right)\right)\right)\left({2}^{nd}\left({J}\left({k}\right)\right)\right)\right)$
10 ovoliun.j ${⊢}{\phi }\to {J}:ℕ\underset{1-1 onto}{⟶}ℕ×ℕ$
11 ovoliun.f ${⊢}{\phi }\to {F}:ℕ⟶{\left(\le \cap {ℝ}^{2}\right)}^{ℕ}$
12 ovoliun.x1 ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\left({n}\right)\right)$
13 ovoliun.x2 ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+\left(\frac{{B}}{{2}^{{n}}}\right)$
14 3 ralrimiva ${⊢}{\phi }\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\subseteq ℝ$
15 iunss ${⊢}\bigcup _{{n}\in ℕ}{A}\subseteq ℝ↔\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\subseteq ℝ$
16 14 15 sylibr ${⊢}{\phi }\to \bigcup _{{n}\in ℕ}{A}\subseteq ℝ$
17 ovolcl ${⊢}\bigcup _{{n}\in ℕ}{A}\subseteq ℝ\to {vol}^{*}\left(\bigcup _{{n}\in ℕ}{A}\right)\in {ℝ}^{*}$
18 16 17 syl ${⊢}{\phi }\to {vol}^{*}\left(\bigcup _{{n}\in ℕ}{A}\right)\in {ℝ}^{*}$
19 11 adantr ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {F}:ℕ⟶{\left(\le \cap {ℝ}^{2}\right)}^{ℕ}$
20 f1of ${⊢}{J}:ℕ\underset{1-1 onto}{⟶}ℕ×ℕ\to {J}:ℕ⟶ℕ×ℕ$
21 10 20 syl ${⊢}{\phi }\to {J}:ℕ⟶ℕ×ℕ$
22 21 ffvelrnda ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {J}\left({k}\right)\in \left(ℕ×ℕ\right)$
23 xp1st ${⊢}{J}\left({k}\right)\in \left(ℕ×ℕ\right)\to {1}^{st}\left({J}\left({k}\right)\right)\in ℕ$
24 22 23 syl ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {1}^{st}\left({J}\left({k}\right)\right)\in ℕ$
25 19 24 ffvelrnd ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {F}\left({1}^{st}\left({J}\left({k}\right)\right)\right)\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)$
26 elovolmlem ${⊢}{F}\left({1}^{st}\left({J}\left({k}\right)\right)\right)\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)↔{F}\left({1}^{st}\left({J}\left({k}\right)\right)\right):ℕ⟶\le \cap {ℝ}^{2}$
27 25 26 sylib ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {F}\left({1}^{st}\left({J}\left({k}\right)\right)\right):ℕ⟶\le \cap {ℝ}^{2}$
28 xp2nd ${⊢}{J}\left({k}\right)\in \left(ℕ×ℕ\right)\to {2}^{nd}\left({J}\left({k}\right)\right)\in ℕ$
29 22 28 syl ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {2}^{nd}\left({J}\left({k}\right)\right)\in ℕ$
30 27 29 ffvelrnd ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {F}\left({1}^{st}\left({J}\left({k}\right)\right)\right)\left({2}^{nd}\left({J}\left({k}\right)\right)\right)\in \left(\le \cap {ℝ}^{2}\right)$
31 30 9 fmptd ${⊢}{\phi }\to {H}:ℕ⟶\le \cap {ℝ}^{2}$
32 eqid ${⊢}\left(\mathrm{abs}\circ -\right)\circ {H}=\left(\mathrm{abs}\circ -\right)\circ {H}$
33 32 8 ovolsf ${⊢}{H}:ℕ⟶\le \cap {ℝ}^{2}\to {U}:ℕ⟶\left[0,\mathrm{+\infty }\right)$
34 frn ${⊢}{U}:ℕ⟶\left[0,\mathrm{+\infty }\right)\to \mathrm{ran}{U}\subseteq \left[0,\mathrm{+\infty }\right)$
35 31 33 34 3syl ${⊢}{\phi }\to \mathrm{ran}{U}\subseteq \left[0,\mathrm{+\infty }\right)$
36 icossxr ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq {ℝ}^{*}$
37 35 36 sstrdi ${⊢}{\phi }\to \mathrm{ran}{U}\subseteq {ℝ}^{*}$
38 supxrcl ${⊢}\mathrm{ran}{U}\subseteq {ℝ}^{*}\to sup\left(\mathrm{ran}{U},{ℝ}^{*},<\right)\in {ℝ}^{*}$
39 37 38 syl ${⊢}{\phi }\to sup\left(\mathrm{ran}{U},{ℝ}^{*},<\right)\in {ℝ}^{*}$
40 6 rpred ${⊢}{\phi }\to {B}\in ℝ$
41 5 40 readdcld ${⊢}{\phi }\to sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{B}\in ℝ$
42 41 rexrd ${⊢}{\phi }\to sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{B}\in {ℝ}^{*}$
43 eliun ${⊢}{z}\in \bigcup _{{n}\in ℕ}{A}↔\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{z}\in {A}$
44 12 3adant3 ${⊢}\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\to {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\left({n}\right)\right)$
45 3 3adant3 ${⊢}\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\to {A}\subseteq ℝ$
46 11 ffvelrnda ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {F}\left({n}\right)\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)$
47 elovolmlem ${⊢}{F}\left({n}\right)\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)↔{F}\left({n}\right):ℕ⟶\le \cap {ℝ}^{2}$
48 46 47 sylib ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {F}\left({n}\right):ℕ⟶\le \cap {ℝ}^{2}$
49 48 3adant3 ${⊢}\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\to {F}\left({n}\right):ℕ⟶\le \cap {ℝ}^{2}$
50 ovolfioo ${⊢}\left({A}\subseteq ℝ\wedge {F}\left({n}\right):ℕ⟶\le \cap {ℝ}^{2}\right)\to \left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\left({n}\right)\right)↔\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({F}\left({n}\right)\left({j}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({F}\left({n}\right)\left({j}\right)\right)\right)\right)$
51 45 49 50 syl2anc ${⊢}\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\to \left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\left({n}\right)\right)↔\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({F}\left({n}\right)\left({j}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({F}\left({n}\right)\left({j}\right)\right)\right)\right)$
52 44 51 mpbid ${⊢}\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\to \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({F}\left({n}\right)\left({j}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({F}\left({n}\right)\left({j}\right)\right)\right)$
53 simp3 ${⊢}\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\to {z}\in {A}$
54 rsp ${⊢}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({F}\left({n}\right)\left({j}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({F}\left({n}\right)\left({j}\right)\right)\right)\to \left({z}\in {A}\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({F}\left({n}\right)\left({j}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({F}\left({n}\right)\left({j}\right)\right)\right)\right)$
55 52 53 54 sylc ${⊢}\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({F}\left({n}\right)\left({j}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({F}\left({n}\right)\left({j}\right)\right)\right)$
56 simpl1 ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\wedge {j}\in ℕ\right)\to {\phi }$
57 f1ocnv ${⊢}{J}:ℕ\underset{1-1 onto}{⟶}ℕ×ℕ\to {{J}}^{-1}:ℕ×ℕ\underset{1-1 onto}{⟶}ℕ$
58 f1of ${⊢}{{J}}^{-1}:ℕ×ℕ\underset{1-1 onto}{⟶}ℕ\to {{J}}^{-1}:ℕ×ℕ⟶ℕ$
59 56 10 57 58 4syl ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\wedge {j}\in ℕ\right)\to {{J}}^{-1}:ℕ×ℕ⟶ℕ$
60 simpl2 ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\wedge {j}\in ℕ\right)\to {n}\in ℕ$
61 simpr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\wedge {j}\in ℕ\right)\to {j}\in ℕ$
62 59 60 61 fovrnd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\wedge {j}\in ℕ\right)\to {n}{{J}}^{-1}{j}\in ℕ$
63 2fveq3 ${⊢}{k}={n}{{J}}^{-1}{j}\to {1}^{st}\left({J}\left({k}\right)\right)={1}^{st}\left({J}\left({n}{{J}}^{-1}{j}\right)\right)$
64 63 fveq2d ${⊢}{k}={n}{{J}}^{-1}{j}\to {F}\left({1}^{st}\left({J}\left({k}\right)\right)\right)={F}\left({1}^{st}\left({J}\left({n}{{J}}^{-1}{j}\right)\right)\right)$
65 2fveq3 ${⊢}{k}={n}{{J}}^{-1}{j}\to {2}^{nd}\left({J}\left({k}\right)\right)={2}^{nd}\left({J}\left({n}{{J}}^{-1}{j}\right)\right)$
66 64 65 fveq12d ${⊢}{k}={n}{{J}}^{-1}{j}\to {F}\left({1}^{st}\left({J}\left({k}\right)\right)\right)\left({2}^{nd}\left({J}\left({k}\right)\right)\right)={F}\left({1}^{st}\left({J}\left({n}{{J}}^{-1}{j}\right)\right)\right)\left({2}^{nd}\left({J}\left({n}{{J}}^{-1}{j}\right)\right)\right)$
67 fvex ${⊢}{F}\left({1}^{st}\left({J}\left({n}{{J}}^{-1}{j}\right)\right)\right)\left({2}^{nd}\left({J}\left({n}{{J}}^{-1}{j}\right)\right)\right)\in \mathrm{V}$
68 66 9 67 fvmpt ${⊢}{n}{{J}}^{-1}{j}\in ℕ\to {H}\left({n}{{J}}^{-1}{j}\right)={F}\left({1}^{st}\left({J}\left({n}{{J}}^{-1}{j}\right)\right)\right)\left({2}^{nd}\left({J}\left({n}{{J}}^{-1}{j}\right)\right)\right)$
69 62 68 syl ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\wedge {j}\in ℕ\right)\to {H}\left({n}{{J}}^{-1}{j}\right)={F}\left({1}^{st}\left({J}\left({n}{{J}}^{-1}{j}\right)\right)\right)\left({2}^{nd}\left({J}\left({n}{{J}}^{-1}{j}\right)\right)\right)$
70 df-ov ${⊢}{n}{{J}}^{-1}{j}={{J}}^{-1}\left(⟨{n},{j}⟩\right)$
71 70 fveq2i ${⊢}{J}\left({n}{{J}}^{-1}{j}\right)={J}\left({{J}}^{-1}\left(⟨{n},{j}⟩\right)\right)$
72 56 10 syl ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\wedge {j}\in ℕ\right)\to {J}:ℕ\underset{1-1 onto}{⟶}ℕ×ℕ$
73 60 61 opelxpd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\wedge {j}\in ℕ\right)\to ⟨{n},{j}⟩\in \left(ℕ×ℕ\right)$
74 f1ocnvfv2 ${⊢}\left({J}:ℕ\underset{1-1 onto}{⟶}ℕ×ℕ\wedge ⟨{n},{j}⟩\in \left(ℕ×ℕ\right)\right)\to {J}\left({{J}}^{-1}\left(⟨{n},{j}⟩\right)\right)=⟨{n},{j}⟩$
75 72 73 74 syl2anc ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\wedge {j}\in ℕ\right)\to {J}\left({{J}}^{-1}\left(⟨{n},{j}⟩\right)\right)=⟨{n},{j}⟩$
76 71 75 syl5eq ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\wedge {j}\in ℕ\right)\to {J}\left({n}{{J}}^{-1}{j}\right)=⟨{n},{j}⟩$
77 76 fveq2d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\wedge {j}\in ℕ\right)\to {1}^{st}\left({J}\left({n}{{J}}^{-1}{j}\right)\right)={1}^{st}\left(⟨{n},{j}⟩\right)$
78 vex ${⊢}{n}\in \mathrm{V}$
79 vex ${⊢}{j}\in \mathrm{V}$
80 78 79 op1st ${⊢}{1}^{st}\left(⟨{n},{j}⟩\right)={n}$
81 77 80 syl6eq ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\wedge {j}\in ℕ\right)\to {1}^{st}\left({J}\left({n}{{J}}^{-1}{j}\right)\right)={n}$
82 81 fveq2d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\wedge {j}\in ℕ\right)\to {F}\left({1}^{st}\left({J}\left({n}{{J}}^{-1}{j}\right)\right)\right)={F}\left({n}\right)$
83 76 fveq2d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\wedge {j}\in ℕ\right)\to {2}^{nd}\left({J}\left({n}{{J}}^{-1}{j}\right)\right)={2}^{nd}\left(⟨{n},{j}⟩\right)$
84 78 79 op2nd ${⊢}{2}^{nd}\left(⟨{n},{j}⟩\right)={j}$
85 83 84 syl6eq ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\wedge {j}\in ℕ\right)\to {2}^{nd}\left({J}\left({n}{{J}}^{-1}{j}\right)\right)={j}$
86 82 85 fveq12d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\wedge {j}\in ℕ\right)\to {F}\left({1}^{st}\left({J}\left({n}{{J}}^{-1}{j}\right)\right)\right)\left({2}^{nd}\left({J}\left({n}{{J}}^{-1}{j}\right)\right)\right)={F}\left({n}\right)\left({j}\right)$
87 69 86 eqtrd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\wedge {j}\in ℕ\right)\to {H}\left({n}{{J}}^{-1}{j}\right)={F}\left({n}\right)\left({j}\right)$
88 87 fveq2d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\wedge {j}\in ℕ\right)\to {1}^{st}\left({H}\left({n}{{J}}^{-1}{j}\right)\right)={1}^{st}\left({F}\left({n}\right)\left({j}\right)\right)$
89 88 breq1d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\wedge {j}\in ℕ\right)\to \left({1}^{st}\left({H}\left({n}{{J}}^{-1}{j}\right)\right)<{z}↔{1}^{st}\left({F}\left({n}\right)\left({j}\right)\right)<{z}\right)$
90 87 fveq2d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\wedge {j}\in ℕ\right)\to {2}^{nd}\left({H}\left({n}{{J}}^{-1}{j}\right)\right)={2}^{nd}\left({F}\left({n}\right)\left({j}\right)\right)$
91 90 breq2d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\wedge {j}\in ℕ\right)\to \left({z}<{2}^{nd}\left({H}\left({n}{{J}}^{-1}{j}\right)\right)↔{z}<{2}^{nd}\left({F}\left({n}\right)\left({j}\right)\right)\right)$
92 89 91 anbi12d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\wedge {j}\in ℕ\right)\to \left(\left({1}^{st}\left({H}\left({n}{{J}}^{-1}{j}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({H}\left({n}{{J}}^{-1}{j}\right)\right)\right)↔\left({1}^{st}\left({F}\left({n}\right)\left({j}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({F}\left({n}\right)\left({j}\right)\right)\right)\right)$
93 92 biimprd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\wedge {j}\in ℕ\right)\to \left(\left({1}^{st}\left({F}\left({n}\right)\left({j}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({F}\left({n}\right)\left({j}\right)\right)\right)\to \left({1}^{st}\left({H}\left({n}{{J}}^{-1}{j}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({H}\left({n}{{J}}^{-1}{j}\right)\right)\right)\right)$
94 2fveq3 ${⊢}{m}={n}{{J}}^{-1}{j}\to {1}^{st}\left({H}\left({m}\right)\right)={1}^{st}\left({H}\left({n}{{J}}^{-1}{j}\right)\right)$
95 94 breq1d ${⊢}{m}={n}{{J}}^{-1}{j}\to \left({1}^{st}\left({H}\left({m}\right)\right)<{z}↔{1}^{st}\left({H}\left({n}{{J}}^{-1}{j}\right)\right)<{z}\right)$
96 2fveq3 ${⊢}{m}={n}{{J}}^{-1}{j}\to {2}^{nd}\left({H}\left({m}\right)\right)={2}^{nd}\left({H}\left({n}{{J}}^{-1}{j}\right)\right)$
97 96 breq2d ${⊢}{m}={n}{{J}}^{-1}{j}\to \left({z}<{2}^{nd}\left({H}\left({m}\right)\right)↔{z}<{2}^{nd}\left({H}\left({n}{{J}}^{-1}{j}\right)\right)\right)$
98 95 97 anbi12d ${⊢}{m}={n}{{J}}^{-1}{j}\to \left(\left({1}^{st}\left({H}\left({m}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({H}\left({m}\right)\right)\right)↔\left({1}^{st}\left({H}\left({n}{{J}}^{-1}{j}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({H}\left({n}{{J}}^{-1}{j}\right)\right)\right)\right)$
99 98 rspcev ${⊢}\left({n}{{J}}^{-1}{j}\in ℕ\wedge \left({1}^{st}\left({H}\left({n}{{J}}^{-1}{j}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({H}\left({n}{{J}}^{-1}{j}\right)\right)\right)\right)\to \exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({H}\left({m}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({H}\left({m}\right)\right)\right)$
100 62 93 99 syl6an ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\wedge {j}\in ℕ\right)\to \left(\left({1}^{st}\left({F}\left({n}\right)\left({j}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({F}\left({n}\right)\left({j}\right)\right)\right)\to \exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({H}\left({m}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({H}\left({m}\right)\right)\right)\right)$
101 100 rexlimdva ${⊢}\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\to \left(\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({F}\left({n}\right)\left({j}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({F}\left({n}\right)\left({j}\right)\right)\right)\to \exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({H}\left({m}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({H}\left({m}\right)\right)\right)\right)$
102 55 101 mpd ${⊢}\left({\phi }\wedge {n}\in ℕ\wedge {z}\in {A}\right)\to \exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({H}\left({m}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({H}\left({m}\right)\right)\right)$
103 102 rexlimdv3a ${⊢}{\phi }\to \left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{z}\in {A}\to \exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({H}\left({m}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({H}\left({m}\right)\right)\right)\right)$
104 43 103 syl5bi ${⊢}{\phi }\to \left({z}\in \bigcup _{{n}\in ℕ}{A}\to \exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({H}\left({m}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({H}\left({m}\right)\right)\right)\right)$
105 104 ralrimiv ${⊢}{\phi }\to \forall {z}\in \bigcup _{{n}\in ℕ}{A}\phantom{\rule{.4em}{0ex}}\exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({H}\left({m}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({H}\left({m}\right)\right)\right)$
106 ovolfioo ${⊢}\left(\bigcup _{{n}\in ℕ}{A}\subseteq ℝ\wedge {H}:ℕ⟶\le \cap {ℝ}^{2}\right)\to \left(\bigcup _{{n}\in ℕ}{A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {H}\right)↔\forall {z}\in \bigcup _{{n}\in ℕ}{A}\phantom{\rule{.4em}{0ex}}\exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({H}\left({m}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({H}\left({m}\right)\right)\right)\right)$
107 16 31 106 syl2anc ${⊢}{\phi }\to \left(\bigcup _{{n}\in ℕ}{A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {H}\right)↔\forall {z}\in \bigcup _{{n}\in ℕ}{A}\phantom{\rule{.4em}{0ex}}\exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({H}\left({m}\right)\right)<{z}\wedge {z}<{2}^{nd}\left({H}\left({m}\right)\right)\right)\right)$
108 105 107 mpbird ${⊢}{\phi }\to \bigcup _{{n}\in ℕ}{A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {H}\right)$
109 8 ovollb ${⊢}\left({H}:ℕ⟶\le \cap {ℝ}^{2}\wedge \bigcup _{{n}\in ℕ}{A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {H}\right)\right)\to {vol}^{*}\left(\bigcup _{{n}\in ℕ}{A}\right)\le sup\left(\mathrm{ran}{U},{ℝ}^{*},<\right)$
110 31 108 109 syl2anc ${⊢}{\phi }\to {vol}^{*}\left(\bigcup _{{n}\in ℕ}{A}\right)\le sup\left(\mathrm{ran}{U},{ℝ}^{*},<\right)$
111 fzfi ${⊢}\left(1\dots {j}\right)\in \mathrm{Fin}$
112 elfznn ${⊢}{w}\in \left(1\dots {j}\right)\to {w}\in ℕ$
113 ffvelrn ${⊢}\left({J}:ℕ⟶ℕ×ℕ\wedge {w}\in ℕ\right)\to {J}\left({w}\right)\in \left(ℕ×ℕ\right)$
114 xp1st ${⊢}{J}\left({w}\right)\in \left(ℕ×ℕ\right)\to {1}^{st}\left({J}\left({w}\right)\right)\in ℕ$
115 nnre ${⊢}{1}^{st}\left({J}\left({w}\right)\right)\in ℕ\to {1}^{st}\left({J}\left({w}\right)\right)\in ℝ$
116 113 114 115 3syl ${⊢}\left({J}:ℕ⟶ℕ×ℕ\wedge {w}\in ℕ\right)\to {1}^{st}\left({J}\left({w}\right)\right)\in ℝ$
117 21 112 116 syl2an ${⊢}\left({\phi }\wedge {w}\in \left(1\dots {j}\right)\right)\to {1}^{st}\left({J}\left({w}\right)\right)\in ℝ$
118 117 ralrimiva ${⊢}{\phi }\to \forall {w}\in \left(1\dots {j}\right)\phantom{\rule{.4em}{0ex}}{1}^{st}\left({J}\left({w}\right)\right)\in ℝ$
119 118 adantr ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to \forall {w}\in \left(1\dots {j}\right)\phantom{\rule{.4em}{0ex}}{1}^{st}\left({J}\left({w}\right)\right)\in ℝ$
120 fimaxre3 ${⊢}\left(\left(1\dots {j}\right)\in \mathrm{Fin}\wedge \forall {w}\in \left(1\dots {j}\right)\phantom{\rule{.4em}{0ex}}{1}^{st}\left({J}\left({w}\right)\right)\in ℝ\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {w}\in \left(1\dots {j}\right)\phantom{\rule{.4em}{0ex}}{1}^{st}\left({J}\left({w}\right)\right)\le {x}$
121 111 119 120 sylancr ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {w}\in \left(1\dots {j}\right)\phantom{\rule{.4em}{0ex}}{1}^{st}\left({J}\left({w}\right)\right)\le {x}$
122 fllep1 ${⊢}{x}\in ℝ\to {x}\le ⌊{x}⌋+1$
123 122 ad2antlr ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {w}\in \left(1\dots {j}\right)\right)\to {x}\le ⌊{x}⌋+1$
124 117 adantlr ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {w}\in \left(1\dots {j}\right)\right)\to {1}^{st}\left({J}\left({w}\right)\right)\in ℝ$
125 simplr ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {w}\in \left(1\dots {j}\right)\right)\to {x}\in ℝ$
126 flcl ${⊢}{x}\in ℝ\to ⌊{x}⌋\in ℤ$
127 126 peano2zd ${⊢}{x}\in ℝ\to ⌊{x}⌋+1\in ℤ$
128 127 zred ${⊢}{x}\in ℝ\to ⌊{x}⌋+1\in ℝ$
129 128 ad2antlr ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {w}\in \left(1\dots {j}\right)\right)\to ⌊{x}⌋+1\in ℝ$
130 letr ${⊢}\left({1}^{st}\left({J}\left({w}\right)\right)\in ℝ\wedge {x}\in ℝ\wedge ⌊{x}⌋+1\in ℝ\right)\to \left(\left({1}^{st}\left({J}\left({w}\right)\right)\le {x}\wedge {x}\le ⌊{x}⌋+1\right)\to {1}^{st}\left({J}\left({w}\right)\right)\le ⌊{x}⌋+1\right)$
131 124 125 129 130 syl3anc ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {w}\in \left(1\dots {j}\right)\right)\to \left(\left({1}^{st}\left({J}\left({w}\right)\right)\le {x}\wedge {x}\le ⌊{x}⌋+1\right)\to {1}^{st}\left({J}\left({w}\right)\right)\le ⌊{x}⌋+1\right)$
132 123 131 mpan2d ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {w}\in \left(1\dots {j}\right)\right)\to \left({1}^{st}\left({J}\left({w}\right)\right)\le {x}\to {1}^{st}\left({J}\left({w}\right)\right)\le ⌊{x}⌋+1\right)$
133 132 ralimdva ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left(\forall {w}\in \left(1\dots {j}\right)\phantom{\rule{.4em}{0ex}}{1}^{st}\left({J}\left({w}\right)\right)\le {x}\to \forall {w}\in \left(1\dots {j}\right)\phantom{\rule{.4em}{0ex}}{1}^{st}\left({J}\left({w}\right)\right)\le ⌊{x}⌋+1\right)$
134 133 adantlr ${⊢}\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge {x}\in ℝ\right)\to \left(\forall {w}\in \left(1\dots {j}\right)\phantom{\rule{.4em}{0ex}}{1}^{st}\left({J}\left({w}\right)\right)\le {x}\to \forall {w}\in \left(1\dots {j}\right)\phantom{\rule{.4em}{0ex}}{1}^{st}\left({J}\left({w}\right)\right)\le ⌊{x}⌋+1\right)$
135 simpll ${⊢}\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge \left({x}\in ℝ\wedge \forall {w}\in \left(1\dots {j}\right)\phantom{\rule{.4em}{0ex}}{1}^{st}\left({J}\left({w}\right)\right)\le ⌊{x}⌋+1\right)\right)\to {\phi }$
136 135 3 sylan ${⊢}\left(\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge \left({x}\in ℝ\wedge \forall {w}\in \left(1\dots {j}\right)\phantom{\rule{.4em}{0ex}}{1}^{st}\left({J}\left({w}\right)\right)\le ⌊{x}⌋+1\right)\right)\wedge {n}\in ℕ\right)\to {A}\subseteq ℝ$
137 135 4 sylan ${⊢}\left(\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge \left({x}\in ℝ\wedge \forall {w}\in \left(1\dots {j}\right)\phantom{\rule{.4em}{0ex}}{1}^{st}\left({J}\left({w}\right)\right)\le ⌊{x}⌋+1\right)\right)\wedge {n}\in ℕ\right)\to {vol}^{*}\left({A}\right)\in ℝ$
138 135 5 syl ${⊢}\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge \left({x}\in ℝ\wedge \forall {w}\in \left(1\dots {j}\right)\phantom{\rule{.4em}{0ex}}{1}^{st}\left({J}\left({w}\right)\right)\le ⌊{x}⌋+1\right)\right)\to sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\in ℝ$
139 135 6 syl ${⊢}\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge \left({x}\in ℝ\wedge \forall {w}\in \left(1\dots {j}\right)\phantom{\rule{.4em}{0ex}}{1}^{st}\left({J}\left({w}\right)\right)\le ⌊{x}⌋+1\right)\right)\to {B}\in {ℝ}^{+}$
140 135 10 syl ${⊢}\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge \left({x}\in ℝ\wedge \forall {w}\in \left(1\dots {j}\right)\phantom{\rule{.4em}{0ex}}{1}^{st}\left({J}\left({w}\right)\right)\le ⌊{x}⌋+1\right)\right)\to {J}:ℕ\underset{1-1 onto}{⟶}ℕ×ℕ$
141 135 11 syl ${⊢}\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge \left({x}\in ℝ\wedge \forall {w}\in \left(1\dots {j}\right)\phantom{\rule{.4em}{0ex}}{1}^{st}\left({J}\left({w}\right)\right)\le ⌊{x}⌋+1\right)\right)\to {F}:ℕ⟶{\left(\le \cap {ℝ}^{2}\right)}^{ℕ}$
142 135 12 sylan ${⊢}\left(\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge \left({x}\in ℝ\wedge \forall {w}\in \left(1\dots {j}\right)\phantom{\rule{.4em}{0ex}}{1}^{st}\left({J}\left({w}\right)\right)\le ⌊{x}⌋+1\right)\right)\wedge {n}\in ℕ\right)\to {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\left({n}\right)\right)$
143 135 13 sylan ${⊢}\left(\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge \left({x}\in ℝ\wedge \forall {w}\in \left(1\dots {j}\right)\phantom{\rule{.4em}{0ex}}{1}^{st}\left({J}\left({w}\right)\right)\le ⌊{x}⌋+1\right)\right)\wedge {n}\in ℕ\right)\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+\left(\frac{{B}}{{2}^{{n}}}\right)$
144 simplr ${⊢}\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge \left({x}\in ℝ\wedge \forall {w}\in \left(1\dots {j}\right)\phantom{\rule{.4em}{0ex}}{1}^{st}\left({J}\left({w}\right)\right)\le ⌊{x}⌋+1\right)\right)\to {j}\in ℕ$
145 127 ad2antrl ${⊢}\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge \left({x}\in ℝ\wedge \forall {w}\in \left(1\dots {j}\right)\phantom{\rule{.4em}{0ex}}{1}^{st}\left({J}\left({w}\right)\right)\le ⌊{x}⌋+1\right)\right)\to ⌊{x}⌋+1\in ℤ$
146 simprr ${⊢}\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge \left({x}\in ℝ\wedge \forall {w}\in \left(1\dots {j}\right)\phantom{\rule{.4em}{0ex}}{1}^{st}\left({J}\left({w}\right)\right)\le ⌊{x}⌋+1\right)\right)\to \forall {w}\in \left(1\dots {j}\right)\phantom{\rule{.4em}{0ex}}{1}^{st}\left({J}\left({w}\right)\right)\le ⌊{x}⌋+1$
147 1 2 136 137 138 139 7 8 9 140 141 142 143 144 145 146 ovoliunlem1 ${⊢}\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge \left({x}\in ℝ\wedge \forall {w}\in \left(1\dots {j}\right)\phantom{\rule{.4em}{0ex}}{1}^{st}\left({J}\left({w}\right)\right)\le ⌊{x}⌋+1\right)\right)\to {U}\left({j}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{B}$
148 147 expr ${⊢}\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge {x}\in ℝ\right)\to \left(\forall {w}\in \left(1\dots {j}\right)\phantom{\rule{.4em}{0ex}}{1}^{st}\left({J}\left({w}\right)\right)\le ⌊{x}⌋+1\to {U}\left({j}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{B}\right)$
149 134 148 syld ${⊢}\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge {x}\in ℝ\right)\to \left(\forall {w}\in \left(1\dots {j}\right)\phantom{\rule{.4em}{0ex}}{1}^{st}\left({J}\left({w}\right)\right)\le {x}\to {U}\left({j}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{B}\right)$
150 149 rexlimdva ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to \left(\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {w}\in \left(1\dots {j}\right)\phantom{\rule{.4em}{0ex}}{1}^{st}\left({J}\left({w}\right)\right)\le {x}\to {U}\left({j}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{B}\right)$
151 121 150 mpd ${⊢}\left({\phi }\wedge {j}\in ℕ\right)\to {U}\left({j}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{B}$
152 151 ralrimiva ${⊢}{\phi }\to \forall {j}\in ℕ\phantom{\rule{.4em}{0ex}}{U}\left({j}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{B}$
153 ffn ${⊢}{U}:ℕ⟶\left[0,\mathrm{+\infty }\right)\to {U}Fnℕ$
154 breq1 ${⊢}{z}={U}\left({j}\right)\to \left({z}\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{B}↔{U}\left({j}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{B}\right)$
155 154 ralrn ${⊢}{U}Fnℕ\to \left(\forall {z}\in \mathrm{ran}{U}\phantom{\rule{.4em}{0ex}}{z}\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{B}↔\forall {j}\in ℕ\phantom{\rule{.4em}{0ex}}{U}\left({j}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{B}\right)$
156 31 33 153 155 4syl ${⊢}{\phi }\to \left(\forall {z}\in \mathrm{ran}{U}\phantom{\rule{.4em}{0ex}}{z}\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{B}↔\forall {j}\in ℕ\phantom{\rule{.4em}{0ex}}{U}\left({j}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{B}\right)$
157 152 156 mpbird ${⊢}{\phi }\to \forall {z}\in \mathrm{ran}{U}\phantom{\rule{.4em}{0ex}}{z}\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{B}$
158 supxrleub ${⊢}\left(\mathrm{ran}{U}\subseteq {ℝ}^{*}\wedge sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{B}\in {ℝ}^{*}\right)\to \left(sup\left(\mathrm{ran}{U},{ℝ}^{*},<\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{B}↔\forall {z}\in \mathrm{ran}{U}\phantom{\rule{.4em}{0ex}}{z}\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{B}\right)$
159 37 42 158 syl2anc ${⊢}{\phi }\to \left(sup\left(\mathrm{ran}{U},{ℝ}^{*},<\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{B}↔\forall {z}\in \mathrm{ran}{U}\phantom{\rule{.4em}{0ex}}{z}\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{B}\right)$
160 157 159 mpbird ${⊢}{\phi }\to sup\left(\mathrm{ran}{U},{ℝ}^{*},<\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{B}$
161 18 39 42 110 160 xrletrd ${⊢}{\phi }\to {vol}^{*}\left(\bigcup _{{n}\in ℕ}{A}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{B}$