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 = seq 1 + G
voliun.2 ⊢ G = n ∈ ℕ ⟼ vol ⁡ A
Assertion voliun ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ Disj n ∈ ℕ A → vol ⁡ ⋃ n ∈ ℕ A = sup ran ⁡ S ℝ * <

Proof

Step Hyp Ref Expression
1 voliun.1 ⊢ S = seq 1 + G
2 voliun.2 ⊢ G = n ∈ ℕ ⟼ vol ⁡ A
3 simpl ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ → A ∈ dom ⁡ vol
4 3 ralimi ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ → ∀ n ∈ ℕ A ∈ dom ⁡ vol
5 4 adantr ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ Disj n ∈ ℕ A → ∀ n ∈ ℕ A ∈ dom ⁡ vol
6 eqid ⊢ n ∈ ℕ ⟼ A = n ∈ ℕ ⟼ A
7 6 fmpt ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ↔ n ∈ ℕ ⟼ A : ℕ ⟶ dom ⁡ vol
8 5 7 sylib ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ Disj n ∈ ℕ A → n ∈ ℕ ⟼ A : ℕ ⟶ dom ⁡ vol
9 6 fvmpt2 ⊢ n ∈ ℕ ∧ A ∈ dom ⁡ vol → n ∈ ℕ ⟼ A ⁡ n = A
10 9 adantrr ⊢ n ∈ ℕ ∧ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ → n ∈ ℕ ⟼ A ⁡ n = A
11 10 ralimiaa ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ → ∀ n ∈ ℕ n ∈ ℕ ⟼ A ⁡ n = A
12 disjeq2 ⊢ ∀ n ∈ ℕ n ∈ ℕ ⟼ A ⁡ n = A → Disj n ∈ ℕ n ∈ ℕ ⟼ A ⁡ n ↔ Disj n ∈ ℕ A
13 11 12 syl ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ → Disj n ∈ ℕ n ∈ ℕ ⟼ A ⁡ n ↔ Disj n ∈ ℕ A
14 13 biimpar ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ Disj n ∈ ℕ A → Disj n ∈ ℕ n ∈ ℕ ⟼ A ⁡ n
15 nfcv ⊢ Ⅎ _ i n ∈ ℕ ⟼ A ⁡ n
16 nffvmpt1 ⊢ Ⅎ _ n n ∈ ℕ ⟼ A ⁡ i
17 fveq2 ⊢ n = i → n ∈ ℕ ⟼ A ⁡ n = n ∈ ℕ ⟼ A ⁡ i
18 15 16 17 cbvdisj ⊢ Disj n ∈ ℕ n ∈ ℕ ⟼ A ⁡ n ↔ Disj i ∈ ℕ n ∈ ℕ ⟼ A ⁡ i
19 14 18 sylib ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ Disj n ∈ ℕ A → Disj i ∈ ℕ n ∈ ℕ ⟼ A ⁡ i
20 eqid ⊢ m ∈ ℕ ⟼ vol * ⁡ x ∩ n ∈ ℕ ⟼ A ⁡ m = m ∈ ℕ ⟼ vol * ⁡ x ∩ n ∈ ℕ ⟼ A ⁡ m
21 eqid ⊢ seq 1 + n ∈ ℕ ⟼ vol ⁡ n ∈ ℕ ⟼ A ⁡ n = seq 1 + n ∈ ℕ ⟼ vol ⁡ n ∈ ℕ ⟼ A ⁡ n
22 nfcv ⊢ Ⅎ _ m vol ⁡ n ∈ ℕ ⟼ A ⁡ n
23 nfcv ⊢ Ⅎ _ n vol
24 nffvmpt1 ⊢ Ⅎ _ n n ∈ ℕ ⟼ A ⁡ m
25 23 24 nffv ⊢ Ⅎ _ n vol ⁡ n ∈ ℕ ⟼ A ⁡ m
26 2fveq3 ⊢ n = m → vol ⁡ n ∈ ℕ ⟼ A ⁡ n = vol ⁡ n ∈ ℕ ⟼ A ⁡ m
27 22 25 26 cbvmpt ⊢ n ∈ ℕ ⟼ vol ⁡ n ∈ ℕ ⟼ A ⁡ n = m ∈ ℕ ⟼ vol ⁡ n ∈ ℕ ⟼ A ⁡ m
28 9 fveq2d ⊢ n ∈ ℕ ∧ A ∈ dom ⁡ vol → vol ⁡ n ∈ ℕ ⟼ A ⁡ n = vol ⁡ A
29 28 eleq1d ⊢ n ∈ ℕ ∧ A ∈ dom ⁡ vol → vol ⁡ n ∈ ℕ ⟼ A ⁡ n ∈ ℝ ↔ vol ⁡ A ∈ ℝ
30 29 biimprd ⊢ n ∈ ℕ ∧ A ∈ dom ⁡ vol → vol ⁡ A ∈ ℝ → vol ⁡ n ∈ ℕ ⟼ A ⁡ n ∈ ℝ
31 30 impr ⊢ n ∈ ℕ ∧ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ → vol ⁡ n ∈ ℕ ⟼ A ⁡ n ∈ ℝ
32 31 ralimiaa ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ → ∀ n ∈ ℕ vol ⁡ n ∈ ℕ ⟼ A ⁡ n ∈ ℝ
33 32 adantr ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ Disj n ∈ ℕ A → ∀ n ∈ ℕ vol ⁡ n ∈ ℕ ⟼ A ⁡ n ∈ ℝ
34 nfv ⊢ Ⅎ i vol ⁡ n ∈ ℕ ⟼ A ⁡ n ∈ ℝ
35 23 16 nffv ⊢ Ⅎ _ n vol ⁡ n ∈ ℕ ⟼ A ⁡ i
36 35 nfel1 ⊢ Ⅎ n vol ⁡ n ∈ ℕ ⟼ A ⁡ i ∈ ℝ
37 2fveq3 ⊢ n = i → vol ⁡ n ∈ ℕ ⟼ A ⁡ n = vol ⁡ n ∈ ℕ ⟼ A ⁡ i
38 37 eleq1d ⊢ n = i → vol ⁡ n ∈ ℕ ⟼ A ⁡ n ∈ ℝ ↔ vol ⁡ n ∈ ℕ ⟼ A ⁡ i ∈ ℝ
39 34 36 38 cbvralw ⊢ ∀ n ∈ ℕ vol ⁡ n ∈ ℕ ⟼ A ⁡ n ∈ ℝ ↔ ∀ i ∈ ℕ vol ⁡ n ∈ ℕ ⟼ A ⁡ i ∈ ℝ
40 33 39 sylib ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ Disj n ∈ ℕ A → ∀ i ∈ ℕ vol ⁡ n ∈ ℕ ⟼ A ⁡ i ∈ ℝ
41 8 19 20 21 27 40 voliunlem3 ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ Disj n ∈ ℕ A → vol ⁡ ⋃ ran ⁡ n ∈ ℕ ⟼ A = sup ran ⁡ seq 1 + n ∈ ℕ ⟼ vol ⁡ n ∈ ℕ ⟼ A ⁡ n ℝ * <
42 dfiun2g ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol → ⋃ n ∈ ℕ A = ⋃ x | ∃ n ∈ ℕ x = A
43 5 42 syl ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ Disj n ∈ ℕ A → ⋃ n ∈ ℕ A = ⋃ x | ∃ n ∈ ℕ x = A
44 6 rnmpt ⊢ ran ⁡ n ∈ ℕ ⟼ A = x | ∃ n ∈ ℕ x = A
45 44 unieqi ⊢ ⋃ ran ⁡ n ∈ ℕ ⟼ A = ⋃ x | ∃ n ∈ ℕ x = A
46 43 45 eqtr4di ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ Disj n ∈ ℕ A → ⋃ n ∈ ℕ A = ⋃ ran ⁡ n ∈ ℕ ⟼ A
47 46 fveq2d ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ Disj n ∈ ℕ A → vol ⁡ ⋃ n ∈ ℕ A = vol ⁡ ⋃ ran ⁡ n ∈ ℕ ⟼ A
48 eqid ⊢ ℕ = ℕ
49 28 adantrr ⊢ n ∈ ℕ ∧ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ → vol ⁡ n ∈ ℕ ⟼ A ⁡ n = vol ⁡ A
50 49 ralimiaa ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ → ∀ n ∈ ℕ vol ⁡ n ∈ ℕ ⟼ A ⁡ n = vol ⁡ A
51 50 adantr ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ Disj n ∈ ℕ A → ∀ n ∈ ℕ vol ⁡ n ∈ ℕ ⟼ A ⁡ n = vol ⁡ A
52 mpteq12 ⊢ ℕ = ℕ ∧ ∀ n ∈ ℕ vol ⁡ n ∈ ℕ ⟼ A ⁡ n = vol ⁡ A → n ∈ ℕ ⟼ vol ⁡ n ∈ ℕ ⟼ A ⁡ n = n ∈ ℕ ⟼ vol ⁡ A
53 48 51 52 sylancr ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ Disj n ∈ ℕ A → n ∈ ℕ ⟼ vol ⁡ n ∈ ℕ ⟼ A ⁡ n = n ∈ ℕ ⟼ vol ⁡ A
54 2 53 eqtr4id ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ Disj n ∈ ℕ A → G = n ∈ ℕ ⟼ vol ⁡ n ∈ ℕ ⟼ A ⁡ n
55 54 seqeq3d ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ Disj n ∈ ℕ A → seq 1 + G = seq 1 + n ∈ ℕ ⟼ vol ⁡ n ∈ ℕ ⟼ A ⁡ n
56 1 55 syl5eq ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ Disj n ∈ ℕ A → S = seq 1 + n ∈ ℕ ⟼ vol ⁡ n ∈ ℕ ⟼ A ⁡ n
57 56 rneqd ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ Disj n ∈ ℕ A → ran ⁡ S = ran ⁡ seq 1 + n ∈ ℕ ⟼ vol ⁡ n ∈ ℕ ⟼ A ⁡ n
58 57 supeq1d ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ Disj n ∈ ℕ A → sup ran ⁡ S ℝ * < = sup ran ⁡ seq 1 + n ∈ ℕ ⟼ vol ⁡ n ∈ ℕ ⟼ A ⁡ n ℝ * <
59 41 47 58 3eqtr4d ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ Disj n ∈ ℕ A → vol ⁡ ⋃ n ∈ ℕ A = sup ran ⁡ S ℝ * <