# Metamath Proof Explorer

## Theorem voliunlem2

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)$
Assertion voliunlem2 ${⊢}{\phi }\to \bigcup \mathrm{ran}{F}\in \mathrm{dom}vol$

### 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 1 frnd ${⊢}{\phi }\to \mathrm{ran}{F}\subseteq \mathrm{dom}vol$
5 mblss ${⊢}{x}\in \mathrm{dom}vol\to {x}\subseteq ℝ$
6 velpw ${⊢}{x}\in 𝒫ℝ↔{x}\subseteq ℝ$
7 5 6 sylibr ${⊢}{x}\in \mathrm{dom}vol\to {x}\in 𝒫ℝ$
8 7 ssriv ${⊢}\mathrm{dom}vol\subseteq 𝒫ℝ$
9 4 8 sstrdi ${⊢}{\phi }\to \mathrm{ran}{F}\subseteq 𝒫ℝ$
10 sspwuni ${⊢}\mathrm{ran}{F}\subseteq 𝒫ℝ↔\bigcup \mathrm{ran}{F}\subseteq ℝ$
11 9 10 sylib ${⊢}{\phi }\to \bigcup \mathrm{ran}{F}\subseteq ℝ$
12 elpwi ${⊢}{x}\in 𝒫ℝ\to {x}\subseteq ℝ$
13 inundif ${⊢}\left({x}\cap \bigcup \mathrm{ran}{F}\right)\cup \left({x}\setminus \bigcup \mathrm{ran}{F}\right)={x}$
14 13 fveq2i ${⊢}{vol}^{*}\left(\left({x}\cap \bigcup \mathrm{ran}{F}\right)\cup \left({x}\setminus \bigcup \mathrm{ran}{F}\right)\right)={vol}^{*}\left({x}\right)$
15 inss1 ${⊢}{x}\cap \bigcup \mathrm{ran}{F}\subseteq {x}$
16 simp2 ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {x}\subseteq ℝ$
17 15 16 sstrid ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {x}\cap \bigcup \mathrm{ran}{F}\subseteq ℝ$
18 ovolsscl ${⊢}\left({x}\cap \bigcup \mathrm{ran}{F}\subseteq {x}\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {vol}^{*}\left({x}\cap \bigcup \mathrm{ran}{F}\right)\in ℝ$
19 15 18 mp3an1 ${⊢}\left({x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {vol}^{*}\left({x}\cap \bigcup \mathrm{ran}{F}\right)\in ℝ$
20 19 3adant1 ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {vol}^{*}\left({x}\cap \bigcup \mathrm{ran}{F}\right)\in ℝ$
21 difss ${⊢}{x}\setminus \bigcup \mathrm{ran}{F}\subseteq {x}$
22 21 16 sstrid ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {x}\setminus \bigcup \mathrm{ran}{F}\subseteq ℝ$
23 ovolsscl ${⊢}\left({x}\setminus \bigcup \mathrm{ran}{F}\subseteq {x}\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\in ℝ$
24 21 23 mp3an1 ${⊢}\left({x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\in ℝ$
25 24 3adant1 ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\in ℝ$
26 ovolun ${⊢}\left(\left({x}\cap \bigcup \mathrm{ran}{F}\subseteq ℝ\wedge {vol}^{*}\left({x}\cap \bigcup \mathrm{ran}{F}\right)\in ℝ\right)\wedge \left({x}\setminus \bigcup \mathrm{ran}{F}\subseteq ℝ\wedge {vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\in ℝ\right)\right)\to {vol}^{*}\left(\left({x}\cap \bigcup \mathrm{ran}{F}\right)\cup \left({x}\setminus \bigcup \mathrm{ran}{F}\right)\right)\le {vol}^{*}\left({x}\cap \bigcup \mathrm{ran}{F}\right)+{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)$
27 17 20 22 25 26 syl22anc ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {vol}^{*}\left(\left({x}\cap \bigcup \mathrm{ran}{F}\right)\cup \left({x}\setminus \bigcup \mathrm{ran}{F}\right)\right)\le {vol}^{*}\left({x}\cap \bigcup \mathrm{ran}{F}\right)+{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)$
28 14 27 eqbrtrrid ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {vol}^{*}\left({x}\right)\le {vol}^{*}\left({x}\cap \bigcup \mathrm{ran}{F}\right)+{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)$
29 20 rexrd ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {vol}^{*}\left({x}\cap \bigcup \mathrm{ran}{F}\right)\in {ℝ}^{*}$
30 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
31 1zzd ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to 1\in ℤ$
32 fveq2 ${⊢}{n}={k}\to {F}\left({n}\right)={F}\left({k}\right)$
33 32 ineq2d ${⊢}{n}={k}\to {x}\cap {F}\left({n}\right)={x}\cap {F}\left({k}\right)$
34 33 fveq2d ${⊢}{n}={k}\to {vol}^{*}\left({x}\cap {F}\left({n}\right)\right)={vol}^{*}\left({x}\cap {F}\left({k}\right)\right)$
35 fvex ${⊢}{vol}^{*}\left({x}\cap {F}\left({k}\right)\right)\in \mathrm{V}$
36 34 3 35 fvmpt ${⊢}{k}\in ℕ\to {H}\left({k}\right)={vol}^{*}\left({x}\cap {F}\left({k}\right)\right)$
37 36 adantl ${⊢}\left(\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\wedge {k}\in ℕ\right)\to {H}\left({k}\right)={vol}^{*}\left({x}\cap {F}\left({k}\right)\right)$
38 inss1 ${⊢}{x}\cap {F}\left({k}\right)\subseteq {x}$
39 ovolsscl ${⊢}\left({x}\cap {F}\left({k}\right)\subseteq {x}\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {vol}^{*}\left({x}\cap {F}\left({k}\right)\right)\in ℝ$
40 38 39 mp3an1 ${⊢}\left({x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {vol}^{*}\left({x}\cap {F}\left({k}\right)\right)\in ℝ$
41 40 3adant1 ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {vol}^{*}\left({x}\cap {F}\left({k}\right)\right)\in ℝ$
42 41 adantr ${⊢}\left(\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\wedge {k}\in ℕ\right)\to {vol}^{*}\left({x}\cap {F}\left({k}\right)\right)\in ℝ$
43 37 42 eqeltrd ${⊢}\left(\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\wedge {k}\in ℕ\right)\to {H}\left({k}\right)\in ℝ$
44 30 31 43 serfre ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to seq1\left(+,{H}\right):ℕ⟶ℝ$
45 44 frnd ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to \mathrm{ran}seq1\left(+,{H}\right)\subseteq ℝ$
46 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
47 45 46 sstrdi ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to \mathrm{ran}seq1\left(+,{H}\right)\subseteq {ℝ}^{*}$
48 supxrcl ${⊢}\mathrm{ran}seq1\left(+,{H}\right)\subseteq {ℝ}^{*}\to sup\left(\mathrm{ran}seq1\left(+,{H}\right),{ℝ}^{*},<\right)\in {ℝ}^{*}$
49 47 48 syl ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to sup\left(\mathrm{ran}seq1\left(+,{H}\right),{ℝ}^{*},<\right)\in {ℝ}^{*}$
50 simp3 ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {vol}^{*}\left({x}\right)\in ℝ$
51 50 25 resubcld ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {vol}^{*}\left({x}\right)-{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\in ℝ$
52 51 rexrd ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {vol}^{*}\left({x}\right)-{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\in {ℝ}^{*}$
53 iunin2 ${⊢}\bigcup _{{n}\in ℕ}\left({x}\cap {F}\left({n}\right)\right)={x}\cap \bigcup _{{n}\in ℕ}{F}\left({n}\right)$
54 ffn ${⊢}{F}:ℕ⟶\mathrm{dom}vol\to {F}Fnℕ$
55 fniunfv ${⊢}{F}Fnℕ\to \bigcup _{{n}\in ℕ}{F}\left({n}\right)=\bigcup \mathrm{ran}{F}$
56 1 54 55 3syl ${⊢}{\phi }\to \bigcup _{{n}\in ℕ}{F}\left({n}\right)=\bigcup \mathrm{ran}{F}$
57 56 3ad2ant1 ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to \bigcup _{{n}\in ℕ}{F}\left({n}\right)=\bigcup \mathrm{ran}{F}$
58 57 ineq2d ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {x}\cap \bigcup _{{n}\in ℕ}{F}\left({n}\right)={x}\cap \bigcup \mathrm{ran}{F}$
59 53 58 syl5eq ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to \bigcup _{{n}\in ℕ}\left({x}\cap {F}\left({n}\right)\right)={x}\cap \bigcup \mathrm{ran}{F}$
60 59 fveq2d ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {vol}^{*}\left(\bigcup _{{n}\in ℕ}\left({x}\cap {F}\left({n}\right)\right)\right)={vol}^{*}\left({x}\cap \bigcup \mathrm{ran}{F}\right)$
61 eqid ${⊢}seq1\left(+,{H}\right)=seq1\left(+,{H}\right)$
62 inss1 ${⊢}{x}\cap {F}\left({n}\right)\subseteq {x}$
63 62 16 sstrid ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {x}\cap {F}\left({n}\right)\subseteq ℝ$
64 63 adantr ${⊢}\left(\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\wedge {n}\in ℕ\right)\to {x}\cap {F}\left({n}\right)\subseteq ℝ$
65 ovolsscl ${⊢}\left({x}\cap {F}\left({n}\right)\subseteq {x}\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {vol}^{*}\left({x}\cap {F}\left({n}\right)\right)\in ℝ$
66 62 65 mp3an1 ${⊢}\left({x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {vol}^{*}\left({x}\cap {F}\left({n}\right)\right)\in ℝ$
67 66 3adant1 ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {vol}^{*}\left({x}\cap {F}\left({n}\right)\right)\in ℝ$
68 67 adantr ${⊢}\left(\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\wedge {n}\in ℕ\right)\to {vol}^{*}\left({x}\cap {F}\left({n}\right)\right)\in ℝ$
69 61 3 64 68 ovoliun ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {vol}^{*}\left(\bigcup _{{n}\in ℕ}\left({x}\cap {F}\left({n}\right)\right)\right)\le sup\left(\mathrm{ran}seq1\left(+,{H}\right),{ℝ}^{*},<\right)$
70 60 69 eqbrtrrd ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {vol}^{*}\left({x}\cap \bigcup \mathrm{ran}{F}\right)\le sup\left(\mathrm{ran}seq1\left(+,{H}\right),{ℝ}^{*},<\right)$
71 1 3ad2ant1 ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {F}:ℕ⟶\mathrm{dom}vol$
72 2 3ad2ant1 ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to \underset{{i}\in ℕ}{Disj}{F}\left({i}\right)$
73 71 72 3 16 50 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)$
74 44 ffvelrnda ${⊢}\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)\in ℝ$
75 25 adantr ${⊢}\left(\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\wedge {k}\in ℕ\right)\to {vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\in ℝ$
76 simpl3 ${⊢}\left(\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\wedge {k}\in ℕ\right)\to {vol}^{*}\left({x}\right)\in ℝ$
77 leaddsub ${⊢}\left(seq1\left(+,{H}\right)\left({k}\right)\in ℝ\wedge {vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\in ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to \left(seq1\left(+,{H}\right)\left({k}\right)+{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\le {vol}^{*}\left({x}\right)↔seq1\left(+,{H}\right)\left({k}\right)\le {vol}^{*}\left({x}\right)-{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\right)$
78 74 75 76 77 syl3anc ${⊢}\left(\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\wedge {k}\in ℕ\right)\to \left(seq1\left(+,{H}\right)\left({k}\right)+{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\le {vol}^{*}\left({x}\right)↔seq1\left(+,{H}\right)\left({k}\right)\le {vol}^{*}\left({x}\right)-{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\right)$
79 73 78 mpbid ${⊢}\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)\le {vol}^{*}\left({x}\right)-{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)$
80 79 ralrimiva ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}seq1\left(+,{H}\right)\left({k}\right)\le {vol}^{*}\left({x}\right)-{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)$
81 ffn ${⊢}seq1\left(+,{H}\right):ℕ⟶ℝ\to seq1\left(+,{H}\right)Fnℕ$
82 breq1 ${⊢}{z}=seq1\left(+,{H}\right)\left({k}\right)\to \left({z}\le {vol}^{*}\left({x}\right)-{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)↔seq1\left(+,{H}\right)\left({k}\right)\le {vol}^{*}\left({x}\right)-{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\right)$
83 82 ralrn ${⊢}seq1\left(+,{H}\right)Fnℕ\to \left(\forall {z}\in \mathrm{ran}seq1\left(+,{H}\right)\phantom{\rule{.4em}{0ex}}{z}\le {vol}^{*}\left({x}\right)-{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)↔\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}seq1\left(+,{H}\right)\left({k}\right)\le {vol}^{*}\left({x}\right)-{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\right)$
84 44 81 83 3syl ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to \left(\forall {z}\in \mathrm{ran}seq1\left(+,{H}\right)\phantom{\rule{.4em}{0ex}}{z}\le {vol}^{*}\left({x}\right)-{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)↔\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}seq1\left(+,{H}\right)\left({k}\right)\le {vol}^{*}\left({x}\right)-{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\right)$
85 80 84 mpbird ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to \forall {z}\in \mathrm{ran}seq1\left(+,{H}\right)\phantom{\rule{.4em}{0ex}}{z}\le {vol}^{*}\left({x}\right)-{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)$
86 supxrleub ${⊢}\left(\mathrm{ran}seq1\left(+,{H}\right)\subseteq {ℝ}^{*}\wedge {vol}^{*}\left({x}\right)-{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\in {ℝ}^{*}\right)\to \left(sup\left(\mathrm{ran}seq1\left(+,{H}\right),{ℝ}^{*},<\right)\le {vol}^{*}\left({x}\right)-{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)↔\forall {z}\in \mathrm{ran}seq1\left(+,{H}\right)\phantom{\rule{.4em}{0ex}}{z}\le {vol}^{*}\left({x}\right)-{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\right)$
87 47 52 86 syl2anc ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to \left(sup\left(\mathrm{ran}seq1\left(+,{H}\right),{ℝ}^{*},<\right)\le {vol}^{*}\left({x}\right)-{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)↔\forall {z}\in \mathrm{ran}seq1\left(+,{H}\right)\phantom{\rule{.4em}{0ex}}{z}\le {vol}^{*}\left({x}\right)-{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\right)$
88 85 87 mpbird ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to sup\left(\mathrm{ran}seq1\left(+,{H}\right),{ℝ}^{*},<\right)\le {vol}^{*}\left({x}\right)-{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)$
89 29 49 52 70 88 xrletrd ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {vol}^{*}\left({x}\cap \bigcup \mathrm{ran}{F}\right)\le {vol}^{*}\left({x}\right)-{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)$
90 leaddsub ${⊢}\left({vol}^{*}\left({x}\cap \bigcup \mathrm{ran}{F}\right)\in ℝ\wedge {vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\in ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to \left({vol}^{*}\left({x}\cap \bigcup \mathrm{ran}{F}\right)+{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\le {vol}^{*}\left({x}\right)↔{vol}^{*}\left({x}\cap \bigcup \mathrm{ran}{F}\right)\le {vol}^{*}\left({x}\right)-{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\right)$
91 20 25 50 90 syl3anc ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to \left({vol}^{*}\left({x}\cap \bigcup \mathrm{ran}{F}\right)+{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\le {vol}^{*}\left({x}\right)↔{vol}^{*}\left({x}\cap \bigcup \mathrm{ran}{F}\right)\le {vol}^{*}\left({x}\right)-{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\right)$
92 89 91 mpbird ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {vol}^{*}\left({x}\cap \bigcup \mathrm{ran}{F}\right)+{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\le {vol}^{*}\left({x}\right)$
93 20 25 readdcld ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {vol}^{*}\left({x}\cap \bigcup \mathrm{ran}{F}\right)+{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\in ℝ$
94 50 93 letri3d ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to \left({vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap \bigcup \mathrm{ran}{F}\right)+{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)↔\left({vol}^{*}\left({x}\right)\le {vol}^{*}\left({x}\cap \bigcup \mathrm{ran}{F}\right)+{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\wedge {vol}^{*}\left({x}\cap \bigcup \mathrm{ran}{F}\right)+{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\le {vol}^{*}\left({x}\right)\right)\right)$
95 28 92 94 mpbir2and ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap \bigcup \mathrm{ran}{F}\right)+{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)$
96 95 3expia ${⊢}\left({\phi }\wedge {x}\subseteq ℝ\right)\to \left({vol}^{*}\left({x}\right)\in ℝ\to {vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap \bigcup \mathrm{ran}{F}\right)+{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\right)$
97 12 96 sylan2 ${⊢}\left({\phi }\wedge {x}\in 𝒫ℝ\right)\to \left({vol}^{*}\left({x}\right)\in ℝ\to {vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap \bigcup \mathrm{ran}{F}\right)+{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\right)$
98 97 ralrimiva ${⊢}{\phi }\to \forall {x}\in 𝒫ℝ\phantom{\rule{.4em}{0ex}}\left({vol}^{*}\left({x}\right)\in ℝ\to {vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap \bigcup \mathrm{ran}{F}\right)+{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\right)$
99 ismbl ${⊢}\bigcup \mathrm{ran}{F}\in \mathrm{dom}vol↔\left(\bigcup \mathrm{ran}{F}\subseteq ℝ\wedge \forall {x}\in 𝒫ℝ\phantom{\rule{.4em}{0ex}}\left({vol}^{*}\left({x}\right)\in ℝ\to {vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap \bigcup \mathrm{ran}{F}\right)+{vol}^{*}\left({x}\setminus \bigcup \mathrm{ran}{F}\right)\right)\right)$
100 11 98 99 sylanbrc ${⊢}{\phi }\to \bigcup \mathrm{ran}{F}\in \mathrm{dom}vol$