# Metamath Proof Explorer

## Theorem uniiccvol

Description: An almost-disjoint union of closed intervals (disjoint interiors) has volume equal to the sum of the volume of the intervals. (This proof does not use countable choice, unlike voliun .) (Contributed by Mario Carneiro, 25-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 uniiccvol ${⊢}{\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 ovolficcss ${⊢}{F}:ℕ⟶\le \cap {ℝ}^{2}\to \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\subseteq ℝ$
5 1 4 syl ${⊢}{\phi }\to \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\subseteq ℝ$
6 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 {ℝ}^{*}$
7 5 6 syl ${⊢}{\phi }\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)\in {ℝ}^{*}$
8 eqid ${⊢}\left(\mathrm{abs}\circ -\right)\circ {F}=\left(\mathrm{abs}\circ -\right)\circ {F}$
9 8 3 ovolsf ${⊢}{F}:ℕ⟶\le \cap {ℝ}^{2}\to {S}:ℕ⟶\left[0,\mathrm{+\infty }\right)$
10 1 9 syl ${⊢}{\phi }\to {S}:ℕ⟶\left[0,\mathrm{+\infty }\right)$
11 10 frnd ${⊢}{\phi }\to \mathrm{ran}{S}\subseteq \left[0,\mathrm{+\infty }\right)$
12 icossxr ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq {ℝ}^{*}$
13 11 12 sstrdi ${⊢}{\phi }\to \mathrm{ran}{S}\subseteq {ℝ}^{*}$
14 supxrcl ${⊢}\mathrm{ran}{S}\subseteq {ℝ}^{*}\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in {ℝ}^{*}$
15 13 14 syl ${⊢}{\phi }\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in {ℝ}^{*}$
16 ssid ${⊢}\bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)$
17 3 ovollb2 ${⊢}\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)$
18 1 16 17 sylancl ${⊢}{\phi }\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)$
19 1 2 3 uniioovol ${⊢}{\phi }\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)$
20 ioossicc ${⊢}\left({1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)\right)\subseteq \left[{1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)\right]$
21 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)$
22 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)$
23 20 21 22 3sstr3i ${⊢}\left(.\right)\left(⟨{1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)⟩\right)\subseteq \left[.\right]\left(⟨{1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)⟩\right)$
24 23 a1i ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {x}\in ℕ\right)\to \left(.\right)\left(⟨{1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)⟩\right)\subseteq \left[.\right]\left(⟨{1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)⟩\right)$
25 ffvelrn ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {x}\in ℕ\right)\to {F}\left({x}\right)\in \left(\le \cap {ℝ}^{2}\right)$
26 25 elin2d ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {x}\in ℕ\right)\to {F}\left({x}\right)\in {ℝ}^{2}$
27 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)⟩$
28 26 27 syl ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {x}\in ℕ\right)\to {F}\left({x}\right)=⟨{1}^{st}\left({F}\left({x}\right)\right),{2}^{nd}\left({F}\left({x}\right)\right)⟩$
29 28 fveq2d ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {x}\in ℕ\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)$
30 28 fveq2d ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {x}\in ℕ\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)$
31 24 29 30 3sstr4d ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {x}\in ℕ\right)\to \left(.\right)\left({F}\left({x}\right)\right)\subseteq \left[.\right]\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 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)$
34 31 32 33 3sstr4d ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {x}\in ℕ\right)\to \left(\left(.\right)\circ {F}\right)\left({x}\right)\subseteq \left(\left[.\right]\circ {F}\right)\left({x}\right)$
35 1 34 sylan ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left(\left(.\right)\circ {F}\right)\left({x}\right)\subseteq \left(\left[.\right]\circ {F}\right)\left({x}\right)$
36 35 ralrimiva ${⊢}{\phi }\to \forall {x}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left(.\right)\circ {F}\right)\left({x}\right)\subseteq \left(\left[.\right]\circ {F}\right)\left({x}\right)$
37 ss2iun ${⊢}\forall {x}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left(.\right)\circ {F}\right)\left({x}\right)\subseteq \left(\left[.\right]\circ {F}\right)\left({x}\right)\to \bigcup _{{x}\in ℕ}\left(\left(.\right)\circ {F}\right)\left({x}\right)\subseteq \bigcup _{{x}\in ℕ}\left(\left[.\right]\circ {F}\right)\left({x}\right)$
38 36 37 syl ${⊢}{\phi }\to \bigcup _{{x}\in ℕ}\left(\left(.\right)\circ {F}\right)\left({x}\right)\subseteq \bigcup _{{x}\in ℕ}\left(\left[.\right]\circ {F}\right)\left({x}\right)$
39 ioof ${⊢}\left(.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫ℝ$
40 ffn ${⊢}\left(.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫ℝ\to \left(.\right)Fn\left({ℝ}^{*}×{ℝ}^{*}\right)$
41 39 40 ax-mp ${⊢}\left(.\right)Fn\left({ℝ}^{*}×{ℝ}^{*}\right)$
42 inss2 ${⊢}\le \cap {ℝ}^{2}\subseteq {ℝ}^{2}$
43 rexpssxrxp ${⊢}{ℝ}^{2}\subseteq {ℝ}^{*}×{ℝ}^{*}$
44 42 43 sstri ${⊢}\le \cap {ℝ}^{2}\subseteq {ℝ}^{*}×{ℝ}^{*}$
45 fss ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge \le \cap {ℝ}^{2}\subseteq {ℝ}^{*}×{ℝ}^{*}\right)\to {F}:ℕ⟶{ℝ}^{*}×{ℝ}^{*}$
46 1 44 45 sylancl ${⊢}{\phi }\to {F}:ℕ⟶{ℝ}^{*}×{ℝ}^{*}$
47 fnfco ${⊢}\left(\left(.\right)Fn\left({ℝ}^{*}×{ℝ}^{*}\right)\wedge {F}:ℕ⟶{ℝ}^{*}×{ℝ}^{*}\right)\to \left(\left(.\right)\circ {F}\right)Fnℕ$
48 41 46 47 sylancr ${⊢}{\phi }\to \left(\left(.\right)\circ {F}\right)Fnℕ$
49 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)$
50 48 49 syl ${⊢}{\phi }\to \bigcup _{{x}\in ℕ}\left(\left(.\right)\circ {F}\right)\left({x}\right)=\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)$
51 iccf ${⊢}\left[.\right]:{ℝ}^{*}×{ℝ}^{*}⟶𝒫{ℝ}^{*}$
52 ffn ${⊢}\left[.\right]:{ℝ}^{*}×{ℝ}^{*}⟶𝒫{ℝ}^{*}\to \left[.\right]Fn\left({ℝ}^{*}×{ℝ}^{*}\right)$
53 51 52 ax-mp ${⊢}\left[.\right]Fn\left({ℝ}^{*}×{ℝ}^{*}\right)$
54 fnfco ${⊢}\left(\left[.\right]Fn\left({ℝ}^{*}×{ℝ}^{*}\right)\wedge {F}:ℕ⟶{ℝ}^{*}×{ℝ}^{*}\right)\to \left(\left[.\right]\circ {F}\right)Fnℕ$
55 53 46 54 sylancr ${⊢}{\phi }\to \left(\left[.\right]\circ {F}\right)Fnℕ$
56 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)$
57 55 56 syl ${⊢}{\phi }\to \bigcup _{{x}\in ℕ}\left(\left[.\right]\circ {F}\right)\left({x}\right)=\bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)$
58 38 50 57 3sstr3d ${⊢}{\phi }\to \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)$
59 ovolss ${⊢}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\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 \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)$
60 58 5 59 syl2anc ${⊢}{\phi }\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)$
61 19 60 eqbrtrrd ${⊢}{\phi }\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\le {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)$
62 7 15 18 61 xrletrid ${⊢}{\phi }\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)$