# Metamath Proof Explorer

## Theorem ovoliun

Description: The Lebesgue outer measure function is countably sub-additive. (Many books allow +oo as a value for one of the sets in the sum, but in our setup we can't do arithmetic on infinity, and in any case the volume of a union containing an infinitely large set is already infinitely large by monotonicity ovolss , so we need not consider this case here, although we do allow the sum itself to be infinite.) (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 ℝ$
Assertion ovoliun ${⊢}{\phi }\to {vol}^{*}\left(\bigcup _{{n}\in ℕ}{A}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)$

### 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 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
6 5 a1i ${⊢}{\phi }\to \mathrm{-\infty }\in {ℝ}^{*}$
7 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
8 1zzd ${⊢}{\phi }\to 1\in ℤ$
9 4 2 fmptd ${⊢}{\phi }\to {G}:ℕ⟶ℝ$
10 9 ffvelrnda ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {G}\left({k}\right)\in ℝ$
11 7 8 10 serfre ${⊢}{\phi }\to seq1\left(+,{G}\right):ℕ⟶ℝ$
12 1 feq1i ${⊢}{T}:ℕ⟶ℝ↔seq1\left(+,{G}\right):ℕ⟶ℝ$
13 11 12 sylibr ${⊢}{\phi }\to {T}:ℕ⟶ℝ$
14 1nn ${⊢}1\in ℕ$
15 ffvelrn ${⊢}\left({T}:ℕ⟶ℝ\wedge 1\in ℕ\right)\to {T}\left(1\right)\in ℝ$
16 13 14 15 sylancl ${⊢}{\phi }\to {T}\left(1\right)\in ℝ$
17 16 rexrd ${⊢}{\phi }\to {T}\left(1\right)\in {ℝ}^{*}$
18 13 frnd ${⊢}{\phi }\to \mathrm{ran}{T}\subseteq ℝ$
19 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
20 18 19 sstrdi ${⊢}{\phi }\to \mathrm{ran}{T}\subseteq {ℝ}^{*}$
21 supxrcl ${⊢}\mathrm{ran}{T}\subseteq {ℝ}^{*}\to sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\in {ℝ}^{*}$
22 20 21 syl ${⊢}{\phi }\to sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\in {ℝ}^{*}$
23 16 mnfltd ${⊢}{\phi }\to \mathrm{-\infty }<{T}\left(1\right)$
24 13 ffnd ${⊢}{\phi }\to {T}Fnℕ$
25 fnfvelrn ${⊢}\left({T}Fnℕ\wedge 1\in ℕ\right)\to {T}\left(1\right)\in \mathrm{ran}{T}$
26 24 14 25 sylancl ${⊢}{\phi }\to {T}\left(1\right)\in \mathrm{ran}{T}$
27 supxrub ${⊢}\left(\mathrm{ran}{T}\subseteq {ℝ}^{*}\wedge {T}\left(1\right)\in \mathrm{ran}{T}\right)\to {T}\left(1\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)$
28 20 26 27 syl2anc ${⊢}{\phi }\to {T}\left(1\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)$
29 6 17 22 23 28 xrltletrd ${⊢}{\phi }\to \mathrm{-\infty }
30 xrrebnd ${⊢}sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\in {ℝ}^{*}\to \left(sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\in ℝ↔\left(\mathrm{-\infty }
31 22 30 syl ${⊢}{\phi }\to \left(sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\in ℝ↔\left(\mathrm{-\infty }
32 29 31 mpbirand ${⊢}{\phi }\to \left(sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\in ℝ↔sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)<\mathrm{+\infty }\right)$
33 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{A}$
34 nfcsb1v
35 csbeq1a
36 33 34 35 cbviun
37 36 fveq2i
38 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({A}\right)$
39 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{vol}^{*}$
40 39 34 nffv
41 35 fveq2d
42 38 40 41 cbvmpt
43 2 42 eqtri
44 3 ralrimiva ${⊢}{\phi }\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\subseteq ℝ$
45 nfv ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}{A}\subseteq ℝ$
46 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}ℝ$
47 34 46 nfss
48 35 sseq1d
49 45 47 48 cbvralw
50 44 49 sylib
52 51 r19.21bi
53 4 ralrimiva ${⊢}{\phi }\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({A}\right)\in ℝ$
54 38 nfel1 ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({A}\right)\in ℝ$
55 40 nfel1
56 41 eleq1d
57 54 55 56 cbvralw
58 53 57 sylib
60 59 r19.21bi
61 simplr ${⊢}\left(\left({\phi }\wedge sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\to sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\in ℝ$
62 simpr ${⊢}\left(\left({\phi }\wedge sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\to {x}\in {ℝ}^{+}$
63 1 43 52 60 61 62 ovoliunlem3
64 37 63 eqbrtrid ${⊢}\left(\left({\phi }\wedge sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\to {vol}^{*}\left(\bigcup _{{n}\in ℕ}{A}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{x}$
65 64 ralrimiva ${⊢}\left({\phi }\wedge sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\in ℝ\right)\to \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{vol}^{*}\left(\bigcup _{{n}\in ℕ}{A}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{x}$
66 iunss ${⊢}\bigcup _{{n}\in ℕ}{A}\subseteq ℝ↔\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\subseteq ℝ$
67 44 66 sylibr ${⊢}{\phi }\to \bigcup _{{n}\in ℕ}{A}\subseteq ℝ$
68 ovolcl ${⊢}\bigcup _{{n}\in ℕ}{A}\subseteq ℝ\to {vol}^{*}\left(\bigcup _{{n}\in ℕ}{A}\right)\in {ℝ}^{*}$
69 67 68 syl ${⊢}{\phi }\to {vol}^{*}\left(\bigcup _{{n}\in ℕ}{A}\right)\in {ℝ}^{*}$
70 xralrple ${⊢}\left({vol}^{*}\left(\bigcup _{{n}\in ℕ}{A}\right)\in {ℝ}^{*}\wedge sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\in ℝ\right)\to \left({vol}^{*}\left(\bigcup _{{n}\in ℕ}{A}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)↔\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{vol}^{*}\left(\bigcup _{{n}\in ℕ}{A}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{x}\right)$
71 69 70 sylan ${⊢}\left({\phi }\wedge sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\in ℝ\right)\to \left({vol}^{*}\left(\bigcup _{{n}\in ℕ}{A}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)↔\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{vol}^{*}\left(\bigcup _{{n}\in ℕ}{A}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{x}\right)$
72 65 71 mpbird ${⊢}\left({\phi }\wedge sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\in ℝ\right)\to {vol}^{*}\left(\bigcup _{{n}\in ℕ}{A}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)$
73 72 ex ${⊢}{\phi }\to \left(sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\in ℝ\to {vol}^{*}\left(\bigcup _{{n}\in ℕ}{A}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right)$
74 32 73 sylbird ${⊢}{\phi }\to \left(sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)<\mathrm{+\infty }\to {vol}^{*}\left(\bigcup _{{n}\in ℕ}{A}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right)$
75 nltpnft ${⊢}sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\in {ℝ}^{*}\to \left(sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)=\mathrm{+\infty }↔¬sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)<\mathrm{+\infty }\right)$
76 22 75 syl ${⊢}{\phi }\to \left(sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)=\mathrm{+\infty }↔¬sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)<\mathrm{+\infty }\right)$
77 pnfge ${⊢}{vol}^{*}\left(\bigcup _{{n}\in ℕ}{A}\right)\in {ℝ}^{*}\to {vol}^{*}\left(\bigcup _{{n}\in ℕ}{A}\right)\le \mathrm{+\infty }$
78 69 77 syl ${⊢}{\phi }\to {vol}^{*}\left(\bigcup _{{n}\in ℕ}{A}\right)\le \mathrm{+\infty }$
79 breq2 ${⊢}sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)=\mathrm{+\infty }\to \left({vol}^{*}\left(\bigcup _{{n}\in ℕ}{A}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)↔{vol}^{*}\left(\bigcup _{{n}\in ℕ}{A}\right)\le \mathrm{+\infty }\right)$
80 78 79 syl5ibrcom ${⊢}{\phi }\to \left(sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)=\mathrm{+\infty }\to {vol}^{*}\left(\bigcup _{{n}\in ℕ}{A}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right)$
81 76 80 sylbird ${⊢}{\phi }\to \left(¬sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)<\mathrm{+\infty }\to {vol}^{*}\left(\bigcup _{{n}\in ℕ}{A}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right)$
82 74 81 pm2.61d ${⊢}{\phi }\to {vol}^{*}\left(\bigcup _{{n}\in ℕ}{A}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)$