# Metamath Proof Explorer

## Theorem uniioovol

Description: A disjoint union of open intervals has volume equal to the sum of the volume of the intervals. (This proof does not use countable choice, unlike voliun .) Lemma 565Ca of Fremlin5 p. 213. (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Hypotheses uniioombl.1 ${⊢}{\phi }\to {F}:ℕ⟶\le \cap {ℝ}^{2}$
uniioombl.2 ${⊢}{\phi }\to \underset{{x}\in ℕ}{Disj}\left(.\right)\left({F}\left({x}\right)\right)$
uniioombl.3 ${⊢}{S}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\right)\right)$
Assertion uniioovol ${⊢}{\phi }\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)$

### Proof

Step Hyp Ref Expression
1 uniioombl.1 ${⊢}{\phi }\to {F}:ℕ⟶\le \cap {ℝ}^{2}$
2 uniioombl.2 ${⊢}{\phi }\to \underset{{x}\in ℕ}{Disj}\left(.\right)\left({F}\left({x}\right)\right)$
3 uniioombl.3 ${⊢}{S}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\right)\right)$
4 ioof ${⊢}\left(.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫ℝ$
5 inss2 ${⊢}\le \cap {ℝ}^{2}\subseteq {ℝ}^{2}$
6 rexpssxrxp ${⊢}{ℝ}^{2}\subseteq {ℝ}^{*}×{ℝ}^{*}$
7 5 6 sstri ${⊢}\le \cap {ℝ}^{2}\subseteq {ℝ}^{*}×{ℝ}^{*}$
8 fss ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge \le \cap {ℝ}^{2}\subseteq {ℝ}^{*}×{ℝ}^{*}\right)\to {F}:ℕ⟶{ℝ}^{*}×{ℝ}^{*}$
9 1 7 8 sylancl ${⊢}{\phi }\to {F}:ℕ⟶{ℝ}^{*}×{ℝ}^{*}$
10 fco ${⊢}\left(\left(.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫ℝ\wedge {F}:ℕ⟶{ℝ}^{*}×{ℝ}^{*}\right)\to \left(\left(.\right)\circ {F}\right):ℕ⟶𝒫ℝ$
11 4 9 10 sylancr ${⊢}{\phi }\to \left(\left(.\right)\circ {F}\right):ℕ⟶𝒫ℝ$
12 11 frnd ${⊢}{\phi }\to \mathrm{ran}\left(\left(.\right)\circ {F}\right)\subseteq 𝒫ℝ$
13 sspwuni ${⊢}\mathrm{ran}\left(\left(.\right)\circ {F}\right)\subseteq 𝒫ℝ↔\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\subseteq ℝ$
14 12 13 sylib ${⊢}{\phi }\to \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\subseteq ℝ$
15 ovolcl ${⊢}\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\subseteq ℝ\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\in {ℝ}^{*}$
16 14 15 syl ${⊢}{\phi }\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\in {ℝ}^{*}$
17 eqid ${⊢}\left(\mathrm{abs}\circ -\right)\circ {F}=\left(\mathrm{abs}\circ -\right)\circ {F}$
18 17 3 ovolsf ${⊢}{F}:ℕ⟶\le \cap {ℝ}^{2}\to {S}:ℕ⟶\left[0,\mathrm{+\infty }\right)$
19 frn ${⊢}{S}:ℕ⟶\left[0,\mathrm{+\infty }\right)\to \mathrm{ran}{S}\subseteq \left[0,\mathrm{+\infty }\right)$
20 1 18 19 3syl ${⊢}{\phi }\to \mathrm{ran}{S}\subseteq \left[0,\mathrm{+\infty }\right)$
21 icossxr ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq {ℝ}^{*}$
22 20 21 sstrdi ${⊢}{\phi }\to \mathrm{ran}{S}\subseteq {ℝ}^{*}$
23 supxrcl ${⊢}\mathrm{ran}{S}\subseteq {ℝ}^{*}\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in {ℝ}^{*}$
24 22 23 syl ${⊢}{\phi }\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in {ℝ}^{*}$
25 ssid ${⊢}\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)$
26 3 ovollb ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)$
27 1 25 26 sylancl ${⊢}{\phi }\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)$
28 1 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {F}:ℕ⟶\le \cap {ℝ}^{2}$
29 elfznn ${⊢}{x}\in \left(1\dots {n}\right)\to {x}\in ℕ$
30 17 ovolfsval ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {x}\in ℕ\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ {F}\right)\left({x}\right)={2}^{nd}\left({F}\left({x}\right)\right)-{1}^{st}\left({F}\left({x}\right)\right)$
31 28 29 30 syl2an ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in \left(1\dots {n}\right)\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ {F}\right)\left({x}\right)={2}^{nd}\left({F}\left({x}\right)\right)-{1}^{st}\left({F}\left({x}\right)\right)$
32 fvco3 ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {x}\in ℕ\right)\to \left(\left(.\right)\circ {F}\right)\left({x}\right)=\left(.\right)\left({F}\left({x}\right)\right)$
33 28 29 32 syl2an ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in \left(1\dots {n}\right)\right)\to \left(\left(.\right)\circ {F}\right)\left({x}\right)=\left(.\right)\left({F}\left({x}\right)\right)$
34 ffvelrn ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {x}\in ℕ\right)\to {F}\left({x}\right)\in \left(\le \cap {ℝ}^{2}\right)$
35 28 29 34 syl2an ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in \left(1\dots {n}\right)\right)\to {F}\left({x}\right)\in \left(\le \cap {ℝ}^{2}\right)$
36 35 elin2d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in \left(1\dots {n}\right)\right)\to {F}\left({x}\right)\in {ℝ}^{2}$
37 1st2nd2 ${⊢}{F}\left({x}\right)\in {ℝ}^{2}\to {F}\left({x}\right)=⟨{1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)⟩$
38 36 37 syl ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in \left(1\dots {n}\right)\right)\to {F}\left({x}\right)=⟨{1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)⟩$
39 38 fveq2d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in \left(1\dots {n}\right)\right)\to \left(.\right)\left({F}\left({x}\right)\right)=\left(.\right)\left(⟨{1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)⟩\right)$
40 df-ov ${⊢}\left({1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)\right)=\left(.\right)\left(⟨{1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)⟩\right)$
41 39 40 syl6eqr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in \left(1\dots {n}\right)\right)\to \left(.\right)\left({F}\left({x}\right)\right)=\left({1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)\right)$
42 33 41 eqtrd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in \left(1\dots {n}\right)\right)\to \left(\left(.\right)\circ {F}\right)\left({x}\right)=\left({1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)\right)$
43 ioombl ${⊢}\left({1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)\right)\in \mathrm{dom}vol$
44 42 43 eqeltrdi ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in \left(1\dots {n}\right)\right)\to \left(\left(.\right)\circ {F}\right)\left({x}\right)\in \mathrm{dom}vol$
45 mblvol ${⊢}\left(\left(.\right)\circ {F}\right)\left({x}\right)\in \mathrm{dom}vol\to vol\left(\left(\left(.\right)\circ {F}\right)\left({x}\right)\right)={vol}^{*}\left(\left(\left(.\right)\circ {F}\right)\left({x}\right)\right)$
46 44 45 syl ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in \left(1\dots {n}\right)\right)\to vol\left(\left(\left(.\right)\circ {F}\right)\left({x}\right)\right)={vol}^{*}\left(\left(\left(.\right)\circ {F}\right)\left({x}\right)\right)$
47 42 fveq2d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in \left(1\dots {n}\right)\right)\to {vol}^{*}\left(\left(\left(.\right)\circ {F}\right)\left({x}\right)\right)={vol}^{*}\left(\left({1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)\right)\right)$
48 ovolfcl ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {x}\in ℕ\right)\to \left({1}^{st}\left({F}\left({x}\right)\right)\in ℝ\wedge {2}^{nd}\left({F}\left({x}\right)\right)\in ℝ\wedge {1}^{st}\left({F}\left({x}\right)\right)\le {2}^{nd}\left({F}\left({x}\right)\right)\right)$
49 28 29 48 syl2an ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in \left(1\dots {n}\right)\right)\to \left({1}^{st}\left({F}\left({x}\right)\right)\in ℝ\wedge {2}^{nd}\left({F}\left({x}\right)\right)\in ℝ\wedge {1}^{st}\left({F}\left({x}\right)\right)\le {2}^{nd}\left({F}\left({x}\right)\right)\right)$
50 ovolioo ${⊢}\left({1}^{st}\left({F}\left({x}\right)\right)\in ℝ\wedge {2}^{nd}\left({F}\left({x}\right)\right)\in ℝ\wedge {1}^{st}\left({F}\left({x}\right)\right)\le {2}^{nd}\left({F}\left({x}\right)\right)\right)\to {vol}^{*}\left(\left({1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)\right)\right)={2}^{nd}\left({F}\left({x}\right)\right)-{1}^{st}\left({F}\left({x}\right)\right)$
51 49 50 syl ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in \left(1\dots {n}\right)\right)\to {vol}^{*}\left(\left({1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)\right)\right)={2}^{nd}\left({F}\left({x}\right)\right)-{1}^{st}\left({F}\left({x}\right)\right)$
52 46 47 51 3eqtrd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in \left(1\dots {n}\right)\right)\to vol\left(\left(\left(.\right)\circ {F}\right)\left({x}\right)\right)={2}^{nd}\left({F}\left({x}\right)\right)-{1}^{st}\left({F}\left({x}\right)\right)$
53 31 52 eqtr4d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in \left(1\dots {n}\right)\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ {F}\right)\left({x}\right)=vol\left(\left(\left(.\right)\circ {F}\right)\left({x}\right)\right)$
54 simpr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {n}\in ℕ$
55 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
56 54 55 eleqtrdi ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {n}\in {ℤ}_{\ge 1}$
57 49 simp2d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in \left(1\dots {n}\right)\right)\to {2}^{nd}\left({F}\left({x}\right)\right)\in ℝ$
58 49 simp1d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in \left(1\dots {n}\right)\right)\to {1}^{st}\left({F}\left({x}\right)\right)\in ℝ$
59 57 58 resubcld ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in \left(1\dots {n}\right)\right)\to {2}^{nd}\left({F}\left({x}\right)\right)-{1}^{st}\left({F}\left({x}\right)\right)\in ℝ$
60 52 59 eqeltrd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in \left(1\dots {n}\right)\right)\to vol\left(\left(\left(.\right)\circ {F}\right)\left({x}\right)\right)\in ℝ$
61 60 recnd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in \left(1\dots {n}\right)\right)\to vol\left(\left(\left(.\right)\circ {F}\right)\left({x}\right)\right)\in ℂ$
62 53 56 61 fsumser ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \sum _{{x}=1}^{{n}}vol\left(\left(\left(.\right)\circ {F}\right)\left({x}\right)\right)=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\right)\right)\left({n}\right)$
63 3 fveq1i ${⊢}{S}\left({n}\right)=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\right)\right)\left({n}\right)$
64 62 63 syl6reqr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {S}\left({n}\right)=\sum _{{x}=1}^{{n}}vol\left(\left(\left(.\right)\circ {F}\right)\left({x}\right)\right)$
65 fzfid ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left(1\dots {n}\right)\in \mathrm{Fin}$
66 44 60 jca ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in \left(1\dots {n}\right)\right)\to \left(\left(\left(.\right)\circ {F}\right)\left({x}\right)\in \mathrm{dom}vol\wedge vol\left(\left(\left(.\right)\circ {F}\right)\left({x}\right)\right)\in ℝ\right)$
67 66 ralrimiva ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \forall {x}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\left(\left(.\right)\circ {F}\right)\left({x}\right)\in \mathrm{dom}vol\wedge vol\left(\left(\left(.\right)\circ {F}\right)\left({x}\right)\right)\in ℝ\right)$
68 fz1ssnn ${⊢}\left(1\dots {n}\right)\subseteq ℕ$
69 1 32 sylan ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left(\left(.\right)\circ {F}\right)\left({x}\right)=\left(.\right)\left({F}\left({x}\right)\right)$
70 69 disjeq2dv ${⊢}{\phi }\to \left(\underset{{x}\in ℕ}{Disj}\left(\left(.\right)\circ {F}\right)\left({x}\right)↔\underset{{x}\in ℕ}{Disj}\left(.\right)\left({F}\left({x}\right)\right)\right)$
71 2 70 mpbird ${⊢}{\phi }\to \underset{{x}\in ℕ}{Disj}\left(\left(.\right)\circ {F}\right)\left({x}\right)$
72 71 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \underset{{x}\in ℕ}{Disj}\left(\left(.\right)\circ {F}\right)\left({x}\right)$
73 disjss1 ${⊢}\left(1\dots {n}\right)\subseteq ℕ\to \left(\underset{{x}\in ℕ}{Disj}\left(\left(.\right)\circ {F}\right)\left({x}\right)\to \underset{{x}=1}{\overset{{n}}{Disj}}\left(\left(.\right)\circ {F}\right)\left({x}\right)\right)$
74 68 72 73 mpsyl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \underset{{x}=1}{\overset{{n}}{Disj}}\left(\left(.\right)\circ {F}\right)\left({x}\right)$
75 volfiniun ${⊢}\left(\left(1\dots {n}\right)\in \mathrm{Fin}\wedge \forall {x}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\left(\left(.\right)\circ {F}\right)\left({x}\right)\in \mathrm{dom}vol\wedge vol\left(\left(\left(.\right)\circ {F}\right)\left({x}\right)\right)\in ℝ\right)\wedge \underset{{x}=1}{\overset{{n}}{Disj}}\left(\left(.\right)\circ {F}\right)\left({x}\right)\right)\to vol\left(\bigcup _{{x}=1}^{{n}}\left(\left(.\right)\circ {F}\right)\left({x}\right)\right)=\sum _{{x}=1}^{{n}}vol\left(\left(\left(.\right)\circ {F}\right)\left({x}\right)\right)$
76 65 67 74 75 syl3anc ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to vol\left(\bigcup _{{x}=1}^{{n}}\left(\left(.\right)\circ {F}\right)\left({x}\right)\right)=\sum _{{x}=1}^{{n}}vol\left(\left(\left(.\right)\circ {F}\right)\left({x}\right)\right)$
77 44 ralrimiva ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \forall {x}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\left(.\right)\circ {F}\right)\left({x}\right)\in \mathrm{dom}vol$
78 finiunmbl ${⊢}\left(\left(1\dots {n}\right)\in \mathrm{Fin}\wedge \forall {x}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}\left(\left(.\right)\circ {F}\right)\left({x}\right)\in \mathrm{dom}vol\right)\to \bigcup _{{x}=1}^{{n}}\left(\left(.\right)\circ {F}\right)\left({x}\right)\in \mathrm{dom}vol$
79 65 77 78 syl2anc ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \bigcup _{{x}=1}^{{n}}\left(\left(.\right)\circ {F}\right)\left({x}\right)\in \mathrm{dom}vol$
80 mblvol ${⊢}\bigcup _{{x}=1}^{{n}}\left(\left(.\right)\circ {F}\right)\left({x}\right)\in \mathrm{dom}vol\to vol\left(\bigcup _{{x}=1}^{{n}}\left(\left(.\right)\circ {F}\right)\left({x}\right)\right)={vol}^{*}\left(\bigcup _{{x}=1}^{{n}}\left(\left(.\right)\circ {F}\right)\left({x}\right)\right)$
81 79 80 syl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to vol\left(\bigcup _{{x}=1}^{{n}}\left(\left(.\right)\circ {F}\right)\left({x}\right)\right)={vol}^{*}\left(\bigcup _{{x}=1}^{{n}}\left(\left(.\right)\circ {F}\right)\left({x}\right)\right)$
82 64 76 81 3eqtr2d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {S}\left({n}\right)={vol}^{*}\left(\bigcup _{{x}=1}^{{n}}\left(\left(.\right)\circ {F}\right)\left({x}\right)\right)$
83 iunss1 ${⊢}\left(1\dots {n}\right)\subseteq ℕ\to \bigcup _{{x}=1}^{{n}}\left(\left(.\right)\circ {F}\right)\left({x}\right)\subseteq \bigcup _{{x}\in ℕ}\left(\left(.\right)\circ {F}\right)\left({x}\right)$
84 68 83 mp1i ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \bigcup _{{x}=1}^{{n}}\left(\left(.\right)\circ {F}\right)\left({x}\right)\subseteq \bigcup _{{x}\in ℕ}\left(\left(.\right)\circ {F}\right)\left({x}\right)$
85 11 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left(\left(.\right)\circ {F}\right):ℕ⟶𝒫ℝ$
86 ffn ${⊢}\left(\left(.\right)\circ {F}\right):ℕ⟶𝒫ℝ\to \left(\left(.\right)\circ {F}\right)Fnℕ$
87 fniunfv ${⊢}\left(\left(.\right)\circ {F}\right)Fnℕ\to \bigcup _{{x}\in ℕ}\left(\left(.\right)\circ {F}\right)\left({x}\right)=\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)$
88 85 86 87 3syl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \bigcup _{{x}\in ℕ}\left(\left(.\right)\circ {F}\right)\left({x}\right)=\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)$
89 84 88 sseqtrd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \bigcup _{{x}=1}^{{n}}\left(\left(.\right)\circ {F}\right)\left({x}\right)\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)$
90 14 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\subseteq ℝ$
91 ovolss ${⊢}\left(\bigcup _{{x}=1}^{{n}}\left(\left(.\right)\circ {F}\right)\left({x}\right)\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\wedge \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\subseteq ℝ\right)\to {vol}^{*}\left(\bigcup _{{x}=1}^{{n}}\left(\left(.\right)\circ {F}\right)\left({x}\right)\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)$
92 89 90 91 syl2anc ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {vol}^{*}\left(\bigcup _{{x}=1}^{{n}}\left(\left(.\right)\circ {F}\right)\left({x}\right)\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)$
93 82 92 eqbrtrd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {S}\left({n}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)$
94 93 ralrimiva ${⊢}{\phi }\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{S}\left({n}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)$
95 1 18 syl ${⊢}{\phi }\to {S}:ℕ⟶\left[0,\mathrm{+\infty }\right)$
96 ffn ${⊢}{S}:ℕ⟶\left[0,\mathrm{+\infty }\right)\to {S}Fnℕ$
97 breq1 ${⊢}{y}={S}\left({n}\right)\to \left({y}\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)↔{S}\left({n}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\right)$
98 97 ralrn ${⊢}{S}Fnℕ\to \left(\forall {y}\in \mathrm{ran}{S}\phantom{\rule{.4em}{0ex}}{y}\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)↔\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{S}\left({n}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\right)$
99 95 96 98 3syl ${⊢}{\phi }\to \left(\forall {y}\in \mathrm{ran}{S}\phantom{\rule{.4em}{0ex}}{y}\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)↔\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{S}\left({n}\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\right)$
100 94 99 mpbird ${⊢}{\phi }\to \forall {y}\in \mathrm{ran}{S}\phantom{\rule{.4em}{0ex}}{y}\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)$
101 supxrleub ${⊢}\left(\mathrm{ran}{S}\subseteq {ℝ}^{*}\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\in {ℝ}^{*}\right)\to \left(sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)↔\forall {y}\in \mathrm{ran}{S}\phantom{\rule{.4em}{0ex}}{y}\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\right)$
102 22 16 101 syl2anc ${⊢}{\phi }\to \left(sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)↔\forall {y}\in \mathrm{ran}{S}\phantom{\rule{.4em}{0ex}}{y}\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\right)$
103 100 102 mpbird ${⊢}{\phi }\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)$
104 16 24 27 103 xrletrid ${⊢}{\phi }\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)$