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 ⊢ 𝑆 = seq 1 ( + , 𝐺 )
voliun.2 ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( vol ‘ 𝐴 ) )
Assertion voliun ( ( ∀ 𝑛 ∈ ℕ ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ Disj 𝑛 ∈ ℕ 𝐴 ) → ( vol ‘ ∪ 𝑛 ∈ ℕ 𝐴 ) = sup ( ran 𝑆 , ℝ* , < ) )

Proof

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