# Metamath Proof Explorer

## Theorem voliunlem3

Description: Lemma for voliun . (Contributed by Mario Carneiro, 20-Mar-2014)

Ref Expression
Hypotheses voliunlem.3 ${⊢}{\phi }\to {F}:ℕ⟶\mathrm{dom}vol$
voliunlem.5 ${⊢}{\phi }\to \underset{{i}\in ℕ}{Disj}{F}\left({i}\right)$
voliunlem.6 ${⊢}{H}=\left({n}\in ℕ⟼{vol}^{*}\left({x}\cap {F}\left({n}\right)\right)\right)$
voliunlem3.1 ${⊢}{S}=seq1\left(+,{G}\right)$
voliunlem3.2 ${⊢}{G}=\left({n}\in ℕ⟼vol\left({F}\left({n}\right)\right)\right)$
voliunlem3.4 ${⊢}{\phi }\to \forall {i}\in ℕ\phantom{\rule{.4em}{0ex}}vol\left({F}\left({i}\right)\right)\in ℝ$
Assertion voliunlem3 ${⊢}{\phi }\to vol\left(\bigcup \mathrm{ran}{F}\right)=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)$

### Proof

Step Hyp Ref Expression
1 voliunlem.3 ${⊢}{\phi }\to {F}:ℕ⟶\mathrm{dom}vol$
2 voliunlem.5 ${⊢}{\phi }\to \underset{{i}\in ℕ}{Disj}{F}\left({i}\right)$
3 voliunlem.6 ${⊢}{H}=\left({n}\in ℕ⟼{vol}^{*}\left({x}\cap {F}\left({n}\right)\right)\right)$
4 voliunlem3.1 ${⊢}{S}=seq1\left(+,{G}\right)$
5 voliunlem3.2 ${⊢}{G}=\left({n}\in ℕ⟼vol\left({F}\left({n}\right)\right)\right)$
6 voliunlem3.4 ${⊢}{\phi }\to \forall {i}\in ℕ\phantom{\rule{.4em}{0ex}}vol\left({F}\left({i}\right)\right)\in ℝ$
7 1 2 3 voliunlem2 ${⊢}{\phi }\to \bigcup \mathrm{ran}{F}\in \mathrm{dom}vol$
8 mblvol ${⊢}\bigcup \mathrm{ran}{F}\in \mathrm{dom}vol\to vol\left(\bigcup \mathrm{ran}{F}\right)={vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)$
9 7 8 syl ${⊢}{\phi }\to vol\left(\bigcup \mathrm{ran}{F}\right)={vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)$
10 1 frnd ${⊢}{\phi }\to \mathrm{ran}{F}\subseteq \mathrm{dom}vol$
11 mblss ${⊢}{x}\in \mathrm{dom}vol\to {x}\subseteq ℝ$
12 reex ${⊢}ℝ\in \mathrm{V}$
13 12 elpw2 ${⊢}{x}\in 𝒫ℝ↔{x}\subseteq ℝ$
14 11 13 sylibr ${⊢}{x}\in \mathrm{dom}vol\to {x}\in 𝒫ℝ$
15 14 ssriv ${⊢}\mathrm{dom}vol\subseteq 𝒫ℝ$
16 10 15 sstrdi ${⊢}{\phi }\to \mathrm{ran}{F}\subseteq 𝒫ℝ$
17 sspwuni ${⊢}\mathrm{ran}{F}\subseteq 𝒫ℝ↔\bigcup \mathrm{ran}{F}\subseteq ℝ$
18 16 17 sylib ${⊢}{\phi }\to \bigcup \mathrm{ran}{F}\subseteq ℝ$
19 ovolcl ${⊢}\bigcup \mathrm{ran}{F}\subseteq ℝ\to {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\in {ℝ}^{*}$
20 18 19 syl ${⊢}{\phi }\to {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\in {ℝ}^{*}$
21 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
22 1zzd ${⊢}{\phi }\to 1\in ℤ$
23 2fveq3 ${⊢}{n}={k}\to vol\left({F}\left({n}\right)\right)=vol\left({F}\left({k}\right)\right)$
24 fvex ${⊢}vol\left({F}\left({k}\right)\right)\in \mathrm{V}$
25 23 5 24 fvmpt ${⊢}{k}\in ℕ\to {G}\left({k}\right)=vol\left({F}\left({k}\right)\right)$
26 25 adantl ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {G}\left({k}\right)=vol\left({F}\left({k}\right)\right)$
27 2fveq3 ${⊢}{i}={k}\to vol\left({F}\left({i}\right)\right)=vol\left({F}\left({k}\right)\right)$
28 27 eleq1d ${⊢}{i}={k}\to \left(vol\left({F}\left({i}\right)\right)\in ℝ↔vol\left({F}\left({k}\right)\right)\in ℝ\right)$
29 28 rspccva ${⊢}\left(\forall {i}\in ℕ\phantom{\rule{.4em}{0ex}}vol\left({F}\left({i}\right)\right)\in ℝ\wedge {k}\in ℕ\right)\to vol\left({F}\left({k}\right)\right)\in ℝ$
30 6 29 sylan ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to vol\left({F}\left({k}\right)\right)\in ℝ$
31 26 30 eqeltrd ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {G}\left({k}\right)\in ℝ$
32 21 22 31 serfre ${⊢}{\phi }\to seq1\left(+,{G}\right):ℕ⟶ℝ$
33 4 feq1i ${⊢}{S}:ℕ⟶ℝ↔seq1\left(+,{G}\right):ℕ⟶ℝ$
34 32 33 sylibr ${⊢}{\phi }\to {S}:ℕ⟶ℝ$
35 34 frnd ${⊢}{\phi }\to \mathrm{ran}{S}\subseteq ℝ$
36 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
37 35 36 sstrdi ${⊢}{\phi }\to \mathrm{ran}{S}\subseteq {ℝ}^{*}$
38 supxrcl ${⊢}\mathrm{ran}{S}\subseteq {ℝ}^{*}\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in {ℝ}^{*}$
39 37 38 syl ${⊢}{\phi }\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in {ℝ}^{*}$
40 eqid ${⊢}seq1\left(+,\left({n}\in ℕ⟼{vol}^{*}\left({F}\left({n}\right)\right)\right)\right)=seq1\left(+,\left({n}\in ℕ⟼{vol}^{*}\left({F}\left({n}\right)\right)\right)\right)$
41 eqid ${⊢}\left({n}\in ℕ⟼{vol}^{*}\left({F}\left({n}\right)\right)\right)=\left({n}\in ℕ⟼{vol}^{*}\left({F}\left({n}\right)\right)\right)$
42 1 ffvelrnda ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {F}\left({n}\right)\in \mathrm{dom}vol$
43 mblss ${⊢}{F}\left({n}\right)\in \mathrm{dom}vol\to {F}\left({n}\right)\subseteq ℝ$
44 42 43 syl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {F}\left({n}\right)\subseteq ℝ$
45 mblvol ${⊢}{F}\left({n}\right)\in \mathrm{dom}vol\to vol\left({F}\left({n}\right)\right)={vol}^{*}\left({F}\left({n}\right)\right)$
46 42 45 syl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to vol\left({F}\left({n}\right)\right)={vol}^{*}\left({F}\left({n}\right)\right)$
47 2fveq3 ${⊢}{i}={n}\to vol\left({F}\left({i}\right)\right)=vol\left({F}\left({n}\right)\right)$
48 47 eleq1d ${⊢}{i}={n}\to \left(vol\left({F}\left({i}\right)\right)\in ℝ↔vol\left({F}\left({n}\right)\right)\in ℝ\right)$
49 48 rspccva ${⊢}\left(\forall {i}\in ℕ\phantom{\rule{.4em}{0ex}}vol\left({F}\left({i}\right)\right)\in ℝ\wedge {n}\in ℕ\right)\to vol\left({F}\left({n}\right)\right)\in ℝ$
50 6 49 sylan ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to vol\left({F}\left({n}\right)\right)\in ℝ$
51 46 50 eqeltrrd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {vol}^{*}\left({F}\left({n}\right)\right)\in ℝ$
52 40 41 44 51 ovoliun ${⊢}{\phi }\to {vol}^{*}\left(\bigcup _{{n}\in ℕ}{F}\left({n}\right)\right)\le sup\left(\mathrm{ran}seq1\left(+,\left({n}\in ℕ⟼{vol}^{*}\left({F}\left({n}\right)\right)\right)\right),{ℝ}^{*},<\right)$
53 1 ffnd ${⊢}{\phi }\to {F}Fnℕ$
54 fniunfv ${⊢}{F}Fnℕ\to \bigcup _{{n}\in ℕ}{F}\left({n}\right)=\bigcup \mathrm{ran}{F}$
55 53 54 syl ${⊢}{\phi }\to \bigcup _{{n}\in ℕ}{F}\left({n}\right)=\bigcup \mathrm{ran}{F}$
56 55 fveq2d ${⊢}{\phi }\to {vol}^{*}\left(\bigcup _{{n}\in ℕ}{F}\left({n}\right)\right)={vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)$
57 46 mpteq2dva ${⊢}{\phi }\to \left({n}\in ℕ⟼vol\left({F}\left({n}\right)\right)\right)=\left({n}\in ℕ⟼{vol}^{*}\left({F}\left({n}\right)\right)\right)$
58 5 57 syl5eq ${⊢}{\phi }\to {G}=\left({n}\in ℕ⟼{vol}^{*}\left({F}\left({n}\right)\right)\right)$
59 58 seqeq3d ${⊢}{\phi }\to seq1\left(+,{G}\right)=seq1\left(+,\left({n}\in ℕ⟼{vol}^{*}\left({F}\left({n}\right)\right)\right)\right)$
60 4 59 syl5req ${⊢}{\phi }\to seq1\left(+,\left({n}\in ℕ⟼{vol}^{*}\left({F}\left({n}\right)\right)\right)\right)={S}$
61 60 rneqd ${⊢}{\phi }\to \mathrm{ran}seq1\left(+,\left({n}\in ℕ⟼{vol}^{*}\left({F}\left({n}\right)\right)\right)\right)=\mathrm{ran}{S}$
62 61 supeq1d ${⊢}{\phi }\to sup\left(\mathrm{ran}seq1\left(+,\left({n}\in ℕ⟼{vol}^{*}\left({F}\left({n}\right)\right)\right)\right),{ℝ}^{*},<\right)=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)$
63 52 56 62 3brtr3d ${⊢}{\phi }\to {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)$
64 ovolge0 ${⊢}\bigcup \mathrm{ran}{F}\subseteq ℝ\to 0\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)$
65 18 64 syl ${⊢}{\phi }\to 0\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)$
66 mnflt0 ${⊢}\mathrm{-\infty }<0$
67 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
68 0xr ${⊢}0\in {ℝ}^{*}$
69 xrltletr ${⊢}\left(\mathrm{-\infty }\in {ℝ}^{*}\wedge 0\in {ℝ}^{*}\wedge {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\in {ℝ}^{*}\right)\to \left(\left(\mathrm{-\infty }<0\wedge 0\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\right)\to \mathrm{-\infty }<{vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\right)$
70 67 68 69 mp3an12 ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\in {ℝ}^{*}\to \left(\left(\mathrm{-\infty }<0\wedge 0\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\right)\to \mathrm{-\infty }<{vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\right)$
71 66 70 mpani ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\in {ℝ}^{*}\to \left(0\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\to \mathrm{-\infty }<{vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\right)$
72 20 65 71 sylc ${⊢}{\phi }\to \mathrm{-\infty }<{vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)$
73 xrrebnd ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\in {ℝ}^{*}\to \left({vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\in ℝ↔\left(\mathrm{-\infty }<{vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)<\mathrm{+\infty }\right)\right)$
74 20 73 syl ${⊢}{\phi }\to \left({vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\in ℝ↔\left(\mathrm{-\infty }<{vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)<\mathrm{+\infty }\right)\right)$
75 12 elpw2 ${⊢}\bigcup \mathrm{ran}{F}\in 𝒫ℝ↔\bigcup \mathrm{ran}{F}\subseteq ℝ$
76 18 75 sylibr ${⊢}{\phi }\to \bigcup \mathrm{ran}{F}\in 𝒫ℝ$
77 simpl ${⊢}\left({x}=\bigcup \mathrm{ran}{F}\wedge {\phi }\right)\to {x}=\bigcup \mathrm{ran}{F}$
78 77 sseq1d ${⊢}\left({x}=\bigcup \mathrm{ran}{F}\wedge {\phi }\right)\to \left({x}\subseteq ℝ↔\bigcup \mathrm{ran}{F}\subseteq ℝ\right)$
79 77 fveq2d ${⊢}\left({x}=\bigcup \mathrm{ran}{F}\wedge {\phi }\right)\to {vol}^{*}\left({x}\right)={vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)$
80 79 eleq1d ${⊢}\left({x}=\bigcup \mathrm{ran}{F}\wedge {\phi }\right)\to \left({vol}^{*}\left({x}\right)\in ℝ↔{vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\in ℝ\right)$
81 simpll ${⊢}\left(\left({x}=\bigcup \mathrm{ran}{F}\wedge {\phi }\right)\wedge {n}\in ℕ\right)\to {x}=\bigcup \mathrm{ran}{F}$
82 81 ineq1d ${⊢}\left(\left({x}=\bigcup \mathrm{ran}{F}\wedge {\phi }\right)\wedge {n}\in ℕ\right)\to {x}\cap {F}\left({n}\right)=\bigcup \mathrm{ran}{F}\cap {F}\left({n}\right)$
83 fnfvelrn ${⊢}\left({F}Fnℕ\wedge {n}\in ℕ\right)\to {F}\left({n}\right)\in \mathrm{ran}{F}$
84 53 83 sylan ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {F}\left({n}\right)\in \mathrm{ran}{F}$
85 elssuni ${⊢}{F}\left({n}\right)\in \mathrm{ran}{F}\to {F}\left({n}\right)\subseteq \bigcup \mathrm{ran}{F}$
86 84 85 syl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {F}\left({n}\right)\subseteq \bigcup \mathrm{ran}{F}$
87 86 adantll ${⊢}\left(\left({x}=\bigcup \mathrm{ran}{F}\wedge {\phi }\right)\wedge {n}\in ℕ\right)\to {F}\left({n}\right)\subseteq \bigcup \mathrm{ran}{F}$
88 sseqin2 ${⊢}{F}\left({n}\right)\subseteq \bigcup \mathrm{ran}{F}↔\bigcup \mathrm{ran}{F}\cap {F}\left({n}\right)={F}\left({n}\right)$
89 87 88 sylib ${⊢}\left(\left({x}=\bigcup \mathrm{ran}{F}\wedge {\phi }\right)\wedge {n}\in ℕ\right)\to \bigcup \mathrm{ran}{F}\cap {F}\left({n}\right)={F}\left({n}\right)$
90 82 89 eqtrd ${⊢}\left(\left({x}=\bigcup \mathrm{ran}{F}\wedge {\phi }\right)\wedge {n}\in ℕ\right)\to {x}\cap {F}\left({n}\right)={F}\left({n}\right)$
91 90 fveq2d ${⊢}\left(\left({x}=\bigcup \mathrm{ran}{F}\wedge {\phi }\right)\wedge {n}\in ℕ\right)\to {vol}^{*}\left({x}\cap {F}\left({n}\right)\right)={vol}^{*}\left({F}\left({n}\right)\right)$
92 46 adantll ${⊢}\left(\left({x}=\bigcup \mathrm{ran}{F}\wedge {\phi }\right)\wedge {n}\in ℕ\right)\to vol\left({F}\left({n}\right)\right)={vol}^{*}\left({F}\left({n}\right)\right)$
93 91 92 eqtr4d ${⊢}\left(\left({x}=\bigcup \mathrm{ran}{F}\wedge {\phi }\right)\wedge {n}\in ℕ\right)\to {vol}^{*}\left({x}\cap {F}\left({n}\right)\right)=vol\left({F}\left({n}\right)\right)$
94 93 mpteq2dva ${⊢}\left({x}=\bigcup \mathrm{ran}{F}\wedge {\phi }\right)\to \left({n}\in ℕ⟼{vol}^{*}\left({x}\cap {F}\left({n}\right)\right)\right)=\left({n}\in ℕ⟼vol\left({F}\left({n}\right)\right)\right)$
95 94 adantrr ${⊢}\left({x}=\bigcup \mathrm{ran}{F}\wedge \left({\phi }\wedge {k}\in ℕ\right)\right)\to \left({n}\in ℕ⟼{vol}^{*}\left({x}\cap {F}\left({n}\right)\right)\right)=\left({n}\in ℕ⟼vol\left({F}\left({n}\right)\right)\right)$
96 95 3 5 3eqtr4g ${⊢}\left({x}=\bigcup \mathrm{ran}{F}\wedge \left({\phi }\wedge {k}\in ℕ\right)\right)\to {H}={G}$
97 96 seqeq3d ${⊢}\left({x}=\bigcup \mathrm{ran}{F}\wedge \left({\phi }\wedge {k}\in ℕ\right)\right)\to seq1\left(+,{H}\right)=seq1\left(+,{G}\right)$
98 97 4 syl6eqr ${⊢}\left({x}=\bigcup \mathrm{ran}{F}\wedge \left({\phi }\wedge {k}\in ℕ\right)\right)\to seq1\left(+,{H}\right)={S}$
99 98 fveq1d ${⊢}\left({x}=\bigcup \mathrm{ran}{F}\wedge \left({\phi }\wedge {k}\in ℕ\right)\right)\to seq1\left(+,{H}\right)\left({k}\right)={S}\left({k}\right)$
100 difeq1 ${⊢}{x}=\bigcup \mathrm{ran}{F}\to {x}\setminus \bigcup \mathrm{ran}{F}=\bigcup \mathrm{ran}{F}\setminus \bigcup \mathrm{ran}{F}$
101 difid ${⊢}\bigcup \mathrm{ran}{F}\setminus \bigcup \mathrm{ran}{F}=\varnothing$
102 100 101 syl6eq ${⊢}{x}=\bigcup \mathrm{ran}{F}\to {x}\setminus \bigcup \mathrm{ran}{F}=\varnothing$
103 102 fveq2d ${⊢}{x}=\bigcup \mathrm{ran}{F}\to {vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)={vol}^{*}\left(\varnothing \right)$
104 ovol0 ${⊢}{vol}^{*}\left(\varnothing \right)=0$
105 103 104 syl6eq ${⊢}{x}=\bigcup \mathrm{ran}{F}\to {vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)=0$
106 105 adantr ${⊢}\left({x}=\bigcup \mathrm{ran}{F}\wedge \left({\phi }\wedge {k}\in ℕ\right)\right)\to {vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)=0$
107 99 106 oveq12d ${⊢}\left({x}=\bigcup \mathrm{ran}{F}\wedge \left({\phi }\wedge {k}\in ℕ\right)\right)\to seq1\left(+,{H}\right)\left({k}\right)+{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)={S}\left({k}\right)+0$
108 34 ffvelrnda ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {S}\left({k}\right)\in ℝ$
109 108 adantl ${⊢}\left({x}=\bigcup \mathrm{ran}{F}\wedge \left({\phi }\wedge {k}\in ℕ\right)\right)\to {S}\left({k}\right)\in ℝ$
110 109 recnd ${⊢}\left({x}=\bigcup \mathrm{ran}{F}\wedge \left({\phi }\wedge {k}\in ℕ\right)\right)\to {S}\left({k}\right)\in ℂ$
111 110 addid1d ${⊢}\left({x}=\bigcup \mathrm{ran}{F}\wedge \left({\phi }\wedge {k}\in ℕ\right)\right)\to {S}\left({k}\right)+0={S}\left({k}\right)$
112 107 111 eqtrd ${⊢}\left({x}=\bigcup \mathrm{ran}{F}\wedge \left({\phi }\wedge {k}\in ℕ\right)\right)\to seq1\left(+,{H}\right)\left({k}\right)+{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)={S}\left({k}\right)$
113 fveq2 ${⊢}{x}=\bigcup \mathrm{ran}{F}\to {vol}^{*}\left({x}\right)={vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)$
114 113 adantr ${⊢}\left({x}=\bigcup \mathrm{ran}{F}\wedge \left({\phi }\wedge {k}\in ℕ\right)\right)\to {vol}^{*}\left({x}\right)={vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)$
115 112 114 breq12d ${⊢}\left({x}=\bigcup \mathrm{ran}{F}\wedge \left({\phi }\wedge {k}\in ℕ\right)\right)\to \left(seq1\left(+,{H}\right)\left({k}\right)+{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\le {vol}^{*}\left({x}\right)↔{S}\left({k}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\right)$
116 115 expr ${⊢}\left({x}=\bigcup \mathrm{ran}{F}\wedge {\phi }\right)\to \left({k}\in ℕ\to \left(seq1\left(+,{H}\right)\left({k}\right)+{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\le {vol}^{*}\left({x}\right)↔{S}\left({k}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\right)\right)$
117 116 pm5.74d ${⊢}\left({x}=\bigcup \mathrm{ran}{F}\wedge {\phi }\right)\to \left(\left({k}\in ℕ\to seq1\left(+,{H}\right)\left({k}\right)+{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\le {vol}^{*}\left({x}\right)\right)↔\left({k}\in ℕ\to {S}\left({k}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\right)\right)$
118 80 117 imbi12d ${⊢}\left({x}=\bigcup \mathrm{ran}{F}\wedge {\phi }\right)\to \left(\left({vol}^{*}\left({x}\right)\in ℝ\to \left({k}\in ℕ\to seq1\left(+,{H}\right)\left({k}\right)+{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\le {vol}^{*}\left({x}\right)\right)\right)↔\left({vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\in ℝ\to \left({k}\in ℕ\to {S}\left({k}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\right)\right)\right)$
119 78 118 imbi12d ${⊢}\left({x}=\bigcup \mathrm{ran}{F}\wedge {\phi }\right)\to \left(\left({x}\subseteq ℝ\to \left({vol}^{*}\left({x}\right)\in ℝ\to \left({k}\in ℕ\to seq1\left(+,{H}\right)\left({k}\right)+{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\le {vol}^{*}\left({x}\right)\right)\right)\right)↔\left(\bigcup \mathrm{ran}{F}\subseteq ℝ\to \left({vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\in ℝ\to \left({k}\in ℕ\to {S}\left({k}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\right)\right)\right)\right)$
120 119 pm5.74da ${⊢}{x}=\bigcup \mathrm{ran}{F}\to \left(\left({\phi }\to \left({x}\subseteq ℝ\to \left({vol}^{*}\left({x}\right)\in ℝ\to \left({k}\in ℕ\to seq1\left(+,{H}\right)\left({k}\right)+{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\le {vol}^{*}\left({x}\right)\right)\right)\right)\right)↔\left({\phi }\to \left(\bigcup \mathrm{ran}{F}\subseteq ℝ\to \left({vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\in ℝ\to \left({k}\in ℕ\to {S}\left({k}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\right)\right)\right)\right)\right)$
121 1 3ad2ant1 ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {F}:ℕ⟶\mathrm{dom}vol$
122 2 3ad2ant1 ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to \underset{{i}\in ℕ}{Disj}{F}\left({i}\right)$
123 simp2 ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {x}\subseteq ℝ$
124 simp3 ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {vol}^{*}\left({x}\right)\in ℝ$
125 121 122 3 123 124 voliunlem1 ${⊢}\left(\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\wedge {k}\in ℕ\right)\to seq1\left(+,{H}\right)\left({k}\right)+{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\le {vol}^{*}\left({x}\right)$
126 125 3exp1 ${⊢}{\phi }\to \left({x}\subseteq ℝ\to \left({vol}^{*}\left({x}\right)\in ℝ\to \left({k}\in ℕ\to seq1\left(+,{H}\right)\left({k}\right)+{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\le {vol}^{*}\left({x}\right)\right)\right)\right)$
127 120 126 vtoclg ${⊢}\bigcup \mathrm{ran}{F}\in 𝒫ℝ\to \left({\phi }\to \left(\bigcup \mathrm{ran}{F}\subseteq ℝ\to \left({vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\in ℝ\to \left({k}\in ℕ\to {S}\left({k}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\right)\right)\right)\right)$
128 76 127 mpcom ${⊢}{\phi }\to \left(\bigcup \mathrm{ran}{F}\subseteq ℝ\to \left({vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\in ℝ\to \left({k}\in ℕ\to {S}\left({k}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\right)\right)\right)$
129 18 128 mpd ${⊢}{\phi }\to \left({vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\in ℝ\to \left({k}\in ℕ\to {S}\left({k}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\right)\right)$
130 74 129 sylbird ${⊢}{\phi }\to \left(\left(\mathrm{-\infty }<{vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)<\mathrm{+\infty }\right)\to \left({k}\in ℕ\to {S}\left({k}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\right)\right)$
131 72 130 mpand ${⊢}{\phi }\to \left({vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)<\mathrm{+\infty }\to \left({k}\in ℕ\to {S}\left({k}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\right)\right)$
132 nltpnft ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\in {ℝ}^{*}\to \left({vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)=\mathrm{+\infty }↔¬{vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)<\mathrm{+\infty }\right)$
133 20 132 syl ${⊢}{\phi }\to \left({vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)=\mathrm{+\infty }↔¬{vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)<\mathrm{+\infty }\right)$
134 rexr ${⊢}{S}\left({k}\right)\in ℝ\to {S}\left({k}\right)\in {ℝ}^{*}$
135 pnfge ${⊢}{S}\left({k}\right)\in {ℝ}^{*}\to {S}\left({k}\right)\le \mathrm{+\infty }$
136 108 134 135 3syl ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {S}\left({k}\right)\le \mathrm{+\infty }$
137 136 ex ${⊢}{\phi }\to \left({k}\in ℕ\to {S}\left({k}\right)\le \mathrm{+\infty }\right)$
138 breq2 ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)=\mathrm{+\infty }\to \left({S}\left({k}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)↔{S}\left({k}\right)\le \mathrm{+\infty }\right)$
139 138 imbi2d ${⊢}{vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)=\mathrm{+\infty }\to \left(\left({k}\in ℕ\to {S}\left({k}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\right)↔\left({k}\in ℕ\to {S}\left({k}\right)\le \mathrm{+\infty }\right)\right)$
140 137 139 syl5ibrcom ${⊢}{\phi }\to \left({vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)=\mathrm{+\infty }\to \left({k}\in ℕ\to {S}\left({k}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\right)\right)$
141 133 140 sylbird ${⊢}{\phi }\to \left(¬{vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)<\mathrm{+\infty }\to \left({k}\in ℕ\to {S}\left({k}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\right)\right)$
142 131 141 pm2.61d ${⊢}{\phi }\to \left({k}\in ℕ\to {S}\left({k}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\right)$
143 142 ralrimiv ${⊢}{\phi }\to \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{S}\left({k}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)$
144 34 ffnd ${⊢}{\phi }\to {S}Fnℕ$
145 breq1 ${⊢}{z}={S}\left({k}\right)\to \left({z}\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)↔{S}\left({k}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\right)$
146 145 ralrn ${⊢}{S}Fnℕ\to \left(\forall {z}\in \mathrm{ran}{S}\phantom{\rule{.4em}{0ex}}{z}\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)↔\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{S}\left({k}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\right)$
147 144 146 syl ${⊢}{\phi }\to \left(\forall {z}\in \mathrm{ran}{S}\phantom{\rule{.4em}{0ex}}{z}\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)↔\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{S}\left({k}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\right)$
148 143 147 mpbird ${⊢}{\phi }\to \forall {z}\in \mathrm{ran}{S}\phantom{\rule{.4em}{0ex}}{z}\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)$
149 supxrleub ${⊢}\left(\mathrm{ran}{S}\subseteq {ℝ}^{*}\wedge {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\in {ℝ}^{*}\right)\to \left(sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)↔\forall {z}\in \mathrm{ran}{S}\phantom{\rule{.4em}{0ex}}{z}\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\right)$
150 37 20 149 syl2anc ${⊢}{\phi }\to \left(sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)↔\forall {z}\in \mathrm{ran}{S}\phantom{\rule{.4em}{0ex}}{z}\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)\right)$
151 148 150 mpbird ${⊢}{\phi }\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)$
152 20 39 63 151 xrletrid ${⊢}{\phi }\to {vol}^{*}\left(\bigcup \mathrm{ran}{F}\right)=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)$
153 9 152 eqtrd ${⊢}{\phi }\to vol\left(\bigcup \mathrm{ran}{F}\right)=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)$