# Metamath Proof Explorer

## Theorem voliun

Description: The Lebesgue measure function is countably additive. (Contributed by Mario Carneiro, 18-Mar-2014) (Proof shortened by Mario Carneiro, 11-Dec-2016)

Ref Expression
Hypotheses voliun.1 ${⊢}{S}=seq1\left(+,{G}\right)$
voliun.2 ${⊢}{G}=\left({n}\in ℕ⟼vol\left({A}\right)\right)$
Assertion voliun ${⊢}\left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}\in \mathrm{dom}vol\wedge vol\left({A}\right)\in ℝ\right)\wedge \underset{{n}\in ℕ}{Disj}{A}\right)\to vol\left(\bigcup _{{n}\in ℕ}{A}\right)=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)$

### Proof

Step Hyp Ref Expression
1 voliun.1 ${⊢}{S}=seq1\left(+,{G}\right)$
2 voliun.2 ${⊢}{G}=\left({n}\in ℕ⟼vol\left({A}\right)\right)$
3 simpl ${⊢}\left({A}\in \mathrm{dom}vol\wedge vol\left({A}\right)\in ℝ\right)\to {A}\in \mathrm{dom}vol$
4 3 ralimi ${⊢}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}\in \mathrm{dom}vol\wedge vol\left({A}\right)\in ℝ\right)\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\in \mathrm{dom}vol$
5 4 adantr ${⊢}\left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}\in \mathrm{dom}vol\wedge vol\left({A}\right)\in ℝ\right)\wedge \underset{{n}\in ℕ}{Disj}{A}\right)\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\in \mathrm{dom}vol$
6 eqid ${⊢}\left({n}\in ℕ⟼{A}\right)=\left({n}\in ℕ⟼{A}\right)$
7 6 fmpt ${⊢}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\in \mathrm{dom}vol↔\left({n}\in ℕ⟼{A}\right):ℕ⟶\mathrm{dom}vol$
8 5 7 sylib ${⊢}\left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}\in \mathrm{dom}vol\wedge vol\left({A}\right)\in ℝ\right)\wedge \underset{{n}\in ℕ}{Disj}{A}\right)\to \left({n}\in ℕ⟼{A}\right):ℕ⟶\mathrm{dom}vol$
9 6 fvmpt2 ${⊢}\left({n}\in ℕ\wedge {A}\in \mathrm{dom}vol\right)\to \left({n}\in ℕ⟼{A}\right)\left({n}\right)={A}$
10 9 adantrr ${⊢}\left({n}\in ℕ\wedge \left({A}\in \mathrm{dom}vol\wedge vol\left({A}\right)\in ℝ\right)\right)\to \left({n}\in ℕ⟼{A}\right)\left({n}\right)={A}$
11 10 ralimiaa ${⊢}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}\in \mathrm{dom}vol\wedge vol\left({A}\right)\in ℝ\right)\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}\in ℕ⟼{A}\right)\left({n}\right)={A}$
12 disjeq2 ${⊢}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}\in ℕ⟼{A}\right)\left({n}\right)={A}\to \left(\underset{{n}\in ℕ}{Disj}\left({n}\in ℕ⟼{A}\right)\left({n}\right)↔\underset{{n}\in ℕ}{Disj}{A}\right)$
13 11 12 syl ${⊢}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}\in \mathrm{dom}vol\wedge vol\left({A}\right)\in ℝ\right)\to \left(\underset{{n}\in ℕ}{Disj}\left({n}\in ℕ⟼{A}\right)\left({n}\right)↔\underset{{n}\in ℕ}{Disj}{A}\right)$
14 13 biimpar ${⊢}\left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}\in \mathrm{dom}vol\wedge vol\left({A}\right)\in ℝ\right)\wedge \underset{{n}\in ℕ}{Disj}{A}\right)\to \underset{{n}\in ℕ}{Disj}\left({n}\in ℕ⟼{A}\right)\left({n}\right)$
15 nfcv ${⊢}\underset{_}{Ⅎ}{i}\phantom{\rule{.4em}{0ex}}\left({n}\in ℕ⟼{A}\right)\left({n}\right)$
16 nffvmpt1 ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\left({n}\in ℕ⟼{A}\right)\left({i}\right)$
17 fveq2 ${⊢}{n}={i}\to \left({n}\in ℕ⟼{A}\right)\left({n}\right)=\left({n}\in ℕ⟼{A}\right)\left({i}\right)$
18 15 16 17 cbvdisj ${⊢}\underset{{n}\in ℕ}{Disj}\left({n}\in ℕ⟼{A}\right)\left({n}\right)↔\underset{{i}\in ℕ}{Disj}\left({n}\in ℕ⟼{A}\right)\left({i}\right)$
19 14 18 sylib ${⊢}\left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}\in \mathrm{dom}vol\wedge vol\left({A}\right)\in ℝ\right)\wedge \underset{{n}\in ℕ}{Disj}{A}\right)\to \underset{{i}\in ℕ}{Disj}\left({n}\in ℕ⟼{A}\right)\left({i}\right)$
20 eqid ${⊢}\left({m}\in ℕ⟼{vol}^{*}\left({x}\cap \left({n}\in ℕ⟼{A}\right)\left({m}\right)\right)\right)=\left({m}\in ℕ⟼{vol}^{*}\left({x}\cap \left({n}\in ℕ⟼{A}\right)\left({m}\right)\right)\right)$
21 eqid ${⊢}seq1\left(+,\left({n}\in ℕ⟼vol\left(\left({n}\in ℕ⟼{A}\right)\left({n}\right)\right)\right)\right)=seq1\left(+,\left({n}\in ℕ⟼vol\left(\left({n}\in ℕ⟼{A}\right)\left({n}\right)\right)\right)\right)$
22 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}vol\left(\left({n}\in ℕ⟼{A}\right)\left({n}\right)\right)$
23 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}vol$
24 nffvmpt1 ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\left({n}\in ℕ⟼{A}\right)\left({m}\right)$
25 23 24 nffv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}vol\left(\left({n}\in ℕ⟼{A}\right)\left({m}\right)\right)$
26 2fveq3 ${⊢}{n}={m}\to vol\left(\left({n}\in ℕ⟼{A}\right)\left({n}\right)\right)=vol\left(\left({n}\in ℕ⟼{A}\right)\left({m}\right)\right)$
27 22 25 26 cbvmpt ${⊢}\left({n}\in ℕ⟼vol\left(\left({n}\in ℕ⟼{A}\right)\left({n}\right)\right)\right)=\left({m}\in ℕ⟼vol\left(\left({n}\in ℕ⟼{A}\right)\left({m}\right)\right)\right)$
28 9 fveq2d ${⊢}\left({n}\in ℕ\wedge {A}\in \mathrm{dom}vol\right)\to vol\left(\left({n}\in ℕ⟼{A}\right)\left({n}\right)\right)=vol\left({A}\right)$
29 28 eleq1d ${⊢}\left({n}\in ℕ\wedge {A}\in \mathrm{dom}vol\right)\to \left(vol\left(\left({n}\in ℕ⟼{A}\right)\left({n}\right)\right)\in ℝ↔vol\left({A}\right)\in ℝ\right)$
30 29 biimprd ${⊢}\left({n}\in ℕ\wedge {A}\in \mathrm{dom}vol\right)\to \left(vol\left({A}\right)\in ℝ\to vol\left(\left({n}\in ℕ⟼{A}\right)\left({n}\right)\right)\in ℝ\right)$
31 30 impr ${⊢}\left({n}\in ℕ\wedge \left({A}\in \mathrm{dom}vol\wedge vol\left({A}\right)\in ℝ\right)\right)\to vol\left(\left({n}\in ℕ⟼{A}\right)\left({n}\right)\right)\in ℝ$
32 31 ralimiaa ${⊢}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}\in \mathrm{dom}vol\wedge vol\left({A}\right)\in ℝ\right)\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}vol\left(\left({n}\in ℕ⟼{A}\right)\left({n}\right)\right)\in ℝ$
33 32 adantr ${⊢}\left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}\in \mathrm{dom}vol\wedge vol\left({A}\right)\in ℝ\right)\wedge \underset{{n}\in ℕ}{Disj}{A}\right)\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}vol\left(\left({n}\in ℕ⟼{A}\right)\left({n}\right)\right)\in ℝ$
34 nfv ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}vol\left(\left({n}\in ℕ⟼{A}\right)\left({n}\right)\right)\in ℝ$
35 23 16 nffv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}vol\left(\left({n}\in ℕ⟼{A}\right)\left({i}\right)\right)$
36 35 nfel1 ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}vol\left(\left({n}\in ℕ⟼{A}\right)\left({i}\right)\right)\in ℝ$
37 2fveq3 ${⊢}{n}={i}\to vol\left(\left({n}\in ℕ⟼{A}\right)\left({n}\right)\right)=vol\left(\left({n}\in ℕ⟼{A}\right)\left({i}\right)\right)$
38 37 eleq1d ${⊢}{n}={i}\to \left(vol\left(\left({n}\in ℕ⟼{A}\right)\left({n}\right)\right)\in ℝ↔vol\left(\left({n}\in ℕ⟼{A}\right)\left({i}\right)\right)\in ℝ\right)$
39 34 36 38 cbvralw ${⊢}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}vol\left(\left({n}\in ℕ⟼{A}\right)\left({n}\right)\right)\in ℝ↔\forall {i}\in ℕ\phantom{\rule{.4em}{0ex}}vol\left(\left({n}\in ℕ⟼{A}\right)\left({i}\right)\right)\in ℝ$
40 33 39 sylib ${⊢}\left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}\in \mathrm{dom}vol\wedge vol\left({A}\right)\in ℝ\right)\wedge \underset{{n}\in ℕ}{Disj}{A}\right)\to \forall {i}\in ℕ\phantom{\rule{.4em}{0ex}}vol\left(\left({n}\in ℕ⟼{A}\right)\left({i}\right)\right)\in ℝ$
41 8 19 20 21 27 40 voliunlem3 ${⊢}\left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}\in \mathrm{dom}vol\wedge vol\left({A}\right)\in ℝ\right)\wedge \underset{{n}\in ℕ}{Disj}{A}\right)\to vol\left(\bigcup \mathrm{ran}\left({n}\in ℕ⟼{A}\right)\right)=sup\left(\mathrm{ran}seq1\left(+,\left({n}\in ℕ⟼vol\left(\left({n}\in ℕ⟼{A}\right)\left({n}\right)\right)\right)\right),{ℝ}^{*},<\right)$
42 dfiun2g ${⊢}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\in \mathrm{dom}vol\to \bigcup _{{n}\in ℕ}{A}=\bigcup \left\{{x}|\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={A}\right\}$
43 5 42 syl ${⊢}\left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}\in \mathrm{dom}vol\wedge vol\left({A}\right)\in ℝ\right)\wedge \underset{{n}\in ℕ}{Disj}{A}\right)\to \bigcup _{{n}\in ℕ}{A}=\bigcup \left\{{x}|\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={A}\right\}$
44 6 rnmpt ${⊢}\mathrm{ran}\left({n}\in ℕ⟼{A}\right)=\left\{{x}|\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={A}\right\}$
45 44 unieqi ${⊢}\bigcup \mathrm{ran}\left({n}\in ℕ⟼{A}\right)=\bigcup \left\{{x}|\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={A}\right\}$
46 43 45 syl6eqr ${⊢}\left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}\in \mathrm{dom}vol\wedge vol\left({A}\right)\in ℝ\right)\wedge \underset{{n}\in ℕ}{Disj}{A}\right)\to \bigcup _{{n}\in ℕ}{A}=\bigcup \mathrm{ran}\left({n}\in ℕ⟼{A}\right)$
47 46 fveq2d ${⊢}\left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}\in \mathrm{dom}vol\wedge vol\left({A}\right)\in ℝ\right)\wedge \underset{{n}\in ℕ}{Disj}{A}\right)\to vol\left(\bigcup _{{n}\in ℕ}{A}\right)=vol\left(\bigcup \mathrm{ran}\left({n}\in ℕ⟼{A}\right)\right)$
48 eqid ${⊢}ℕ=ℕ$
49 28 adantrr ${⊢}\left({n}\in ℕ\wedge \left({A}\in \mathrm{dom}vol\wedge vol\left({A}\right)\in ℝ\right)\right)\to vol\left(\left({n}\in ℕ⟼{A}\right)\left({n}\right)\right)=vol\left({A}\right)$
50 49 ralimiaa ${⊢}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}\in \mathrm{dom}vol\wedge vol\left({A}\right)\in ℝ\right)\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}vol\left(\left({n}\in ℕ⟼{A}\right)\left({n}\right)\right)=vol\left({A}\right)$
51 50 adantr ${⊢}\left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}\in \mathrm{dom}vol\wedge vol\left({A}\right)\in ℝ\right)\wedge \underset{{n}\in ℕ}{Disj}{A}\right)\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}vol\left(\left({n}\in ℕ⟼{A}\right)\left({n}\right)\right)=vol\left({A}\right)$
52 mpteq12 ${⊢}\left(ℕ=ℕ\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}vol\left(\left({n}\in ℕ⟼{A}\right)\left({n}\right)\right)=vol\left({A}\right)\right)\to \left({n}\in ℕ⟼vol\left(\left({n}\in ℕ⟼{A}\right)\left({n}\right)\right)\right)=\left({n}\in ℕ⟼vol\left({A}\right)\right)$
53 48 51 52 sylancr ${⊢}\left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}\in \mathrm{dom}vol\wedge vol\left({A}\right)\in ℝ\right)\wedge \underset{{n}\in ℕ}{Disj}{A}\right)\to \left({n}\in ℕ⟼vol\left(\left({n}\in ℕ⟼{A}\right)\left({n}\right)\right)\right)=\left({n}\in ℕ⟼vol\left({A}\right)\right)$
54 53 2 syl6reqr ${⊢}\left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}\in \mathrm{dom}vol\wedge vol\left({A}\right)\in ℝ\right)\wedge \underset{{n}\in ℕ}{Disj}{A}\right)\to {G}=\left({n}\in ℕ⟼vol\left(\left({n}\in ℕ⟼{A}\right)\left({n}\right)\right)\right)$
55 54 seqeq3d ${⊢}\left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}\in \mathrm{dom}vol\wedge vol\left({A}\right)\in ℝ\right)\wedge \underset{{n}\in ℕ}{Disj}{A}\right)\to seq1\left(+,{G}\right)=seq1\left(+,\left({n}\in ℕ⟼vol\left(\left({n}\in ℕ⟼{A}\right)\left({n}\right)\right)\right)\right)$
56 1 55 syl5eq ${⊢}\left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}\in \mathrm{dom}vol\wedge vol\left({A}\right)\in ℝ\right)\wedge \underset{{n}\in ℕ}{Disj}{A}\right)\to {S}=seq1\left(+,\left({n}\in ℕ⟼vol\left(\left({n}\in ℕ⟼{A}\right)\left({n}\right)\right)\right)\right)$
57 56 rneqd ${⊢}\left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}\in \mathrm{dom}vol\wedge vol\left({A}\right)\in ℝ\right)\wedge \underset{{n}\in ℕ}{Disj}{A}\right)\to \mathrm{ran}{S}=\mathrm{ran}seq1\left(+,\left({n}\in ℕ⟼vol\left(\left({n}\in ℕ⟼{A}\right)\left({n}\right)\right)\right)\right)$
58 57 supeq1d ${⊢}\left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}\in \mathrm{dom}vol\wedge vol\left({A}\right)\in ℝ\right)\wedge \underset{{n}\in ℕ}{Disj}{A}\right)\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)=sup\left(\mathrm{ran}seq1\left(+,\left({n}\in ℕ⟼vol\left(\left({n}\in ℕ⟼{A}\right)\left({n}\right)\right)\right)\right),{ℝ}^{*},<\right)$
59 41 47 58 3eqtr4d ${⊢}\left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}\in \mathrm{dom}vol\wedge vol\left({A}\right)\in ℝ\right)\wedge \underset{{n}\in ℕ}{Disj}{A}\right)\to vol\left(\bigcup _{{n}\in ℕ}{A}\right)=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)$