Step |
Hyp |
Ref |
Expression |
1 |
|
meascnbl.0 |
⊢ 𝐽 = ( TopOpen ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) |
2 |
|
meascnbl.1 |
⊢ ( 𝜑 → 𝑀 ∈ ( measures ‘ 𝑆 ) ) |
3 |
|
meascnbl.2 |
⊢ ( 𝜑 → 𝐹 : ℕ ⟶ 𝑆 ) |
4 |
|
meascnbl.3 |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) |
5 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑀 ∈ ( measures ‘ 𝑆 ) ) |
6 |
|
measbase |
⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑆 ∈ ∪ ran sigAlgebra ) |
7 |
2 6
|
syl |
⊢ ( 𝜑 → 𝑆 ∈ ∪ ran sigAlgebra ) |
8 |
7
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑆 ∈ ∪ ran sigAlgebra ) |
9 |
3
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ 𝑆 ) |
10 |
|
simpll |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ..^ 𝑛 ) ) → 𝜑 ) |
11 |
|
fzossnn |
⊢ ( 1 ..^ 𝑛 ) ⊆ ℕ |
12 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ..^ 𝑛 ) ) → 𝑘 ∈ ( 1 ..^ 𝑛 ) ) |
13 |
11 12
|
sselid |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ..^ 𝑛 ) ) → 𝑘 ∈ ℕ ) |
14 |
3
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑆 ) |
15 |
10 13 14
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ..^ 𝑛 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑆 ) |
16 |
15
|
ralrimiva |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∀ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑆 ) |
17 |
|
sigaclfu2 |
⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑆 ) → ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑆 ) |
18 |
8 16 17
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑆 ) |
19 |
|
difelsiga |
⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ( 𝐹 ‘ 𝑛 ) ∈ 𝑆 ∧ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) ∈ 𝑆 ) |
20 |
8 9 18 19
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) ∈ 𝑆 ) |
21 |
|
measvxrge0 |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( ( 𝐹 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) ∈ 𝑆 ) → ( 𝑀 ‘ ( ( 𝐹 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) ) ∈ ( 0 [,] +∞ ) ) |
22 |
5 20 21
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑀 ‘ ( ( 𝐹 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) ) ∈ ( 0 [,] +∞ ) ) |
23 |
|
fveq2 |
⊢ ( 𝑛 = 𝑜 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑜 ) ) |
24 |
|
oveq2 |
⊢ ( 𝑛 = 𝑜 → ( 1 ..^ 𝑛 ) = ( 1 ..^ 𝑜 ) ) |
25 |
24
|
iuneq1d |
⊢ ( 𝑛 = 𝑜 → ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹 ‘ 𝑘 ) = ∪ 𝑘 ∈ ( 1 ..^ 𝑜 ) ( 𝐹 ‘ 𝑘 ) ) |
26 |
23 25
|
difeq12d |
⊢ ( 𝑛 = 𝑜 → ( ( 𝐹 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑜 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑜 ) ( 𝐹 ‘ 𝑘 ) ) ) |
27 |
26
|
fveq2d |
⊢ ( 𝑛 = 𝑜 → ( 𝑀 ‘ ( ( 𝐹 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑀 ‘ ( ( 𝐹 ‘ 𝑜 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑜 ) ( 𝐹 ‘ 𝑘 ) ) ) ) |
28 |
|
fveq2 |
⊢ ( 𝑛 = 𝑝 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑝 ) ) |
29 |
|
oveq2 |
⊢ ( 𝑛 = 𝑝 → ( 1 ..^ 𝑛 ) = ( 1 ..^ 𝑝 ) ) |
30 |
29
|
iuneq1d |
⊢ ( 𝑛 = 𝑝 → ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹 ‘ 𝑘 ) = ∪ 𝑘 ∈ ( 1 ..^ 𝑝 ) ( 𝐹 ‘ 𝑘 ) ) |
31 |
28 30
|
difeq12d |
⊢ ( 𝑛 = 𝑝 → ( ( 𝐹 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑝 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑝 ) ( 𝐹 ‘ 𝑘 ) ) ) |
32 |
31
|
fveq2d |
⊢ ( 𝑛 = 𝑝 → ( 𝑀 ‘ ( ( 𝐹 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑀 ‘ ( ( 𝐹 ‘ 𝑝 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑝 ) ( 𝐹 ‘ 𝑘 ) ) ) ) |
33 |
1 22 27 32
|
esumcvg2 |
⊢ ( 𝜑 → ( 𝑖 ∈ ℕ ↦ Σ* 𝑛 ∈ ( 1 ... 𝑖 ) ( 𝑀 ‘ ( ( 𝐹 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) ) ) ( ⇝𝑡 ‘ 𝐽 ) Σ* 𝑛 ∈ ℕ ( 𝑀 ‘ ( ( 𝐹 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) ) ) |
34 |
|
measfrge0 |
⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) ) |
35 |
2 34
|
syl |
⊢ ( 𝜑 → 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) ) |
36 |
|
fcompt |
⊢ ( ( 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ 𝐹 : ℕ ⟶ 𝑆 ) → ( 𝑀 ∘ 𝐹 ) = ( 𝑖 ∈ ℕ ↦ ( 𝑀 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) |
37 |
35 3 36
|
syl2anc |
⊢ ( 𝜑 → ( 𝑀 ∘ 𝐹 ) = ( 𝑖 ∈ ℕ ↦ ( 𝑀 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) |
38 |
|
nfcv |
⊢ Ⅎ 𝑛 ( 𝐹 ‘ 𝑘 ) |
39 |
|
fveq2 |
⊢ ( 𝑛 = 𝑘 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑘 ) ) |
40 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → 𝑖 ∈ ℕ ) |
41 |
40
|
nnzd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → 𝑖 ∈ ℤ ) |
42 |
|
fzval3 |
⊢ ( 𝑖 ∈ ℤ → ( 1 ... 𝑖 ) = ( 1 ..^ ( 𝑖 + 1 ) ) ) |
43 |
41 42
|
syl |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 1 ... 𝑖 ) = ( 1 ..^ ( 𝑖 + 1 ) ) ) |
44 |
43
|
olcd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( ( 1 ... 𝑖 ) = ℕ ∨ ( 1 ... 𝑖 ) = ( 1 ..^ ( 𝑖 + 1 ) ) ) ) |
45 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → 𝑀 ∈ ( measures ‘ 𝑆 ) ) |
46 |
|
simpll |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑖 ) ) → 𝜑 ) |
47 |
|
fzossnn |
⊢ ( 1 ..^ ( 𝑖 + 1 ) ) ⊆ ℕ |
48 |
43
|
eleq2d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 𝑛 ∈ ( 1 ... 𝑖 ) ↔ 𝑛 ∈ ( 1 ..^ ( 𝑖 + 1 ) ) ) ) |
49 |
48
|
biimpa |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑖 ) ) → 𝑛 ∈ ( 1 ..^ ( 𝑖 + 1 ) ) ) |
50 |
47 49
|
sselid |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑖 ) ) → 𝑛 ∈ ℕ ) |
51 |
46 50 9
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑖 ) ) → ( 𝐹 ‘ 𝑛 ) ∈ 𝑆 ) |
52 |
38 39 44 45 51
|
measiuns |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 𝑀 ‘ ∪ 𝑛 ∈ ( 1 ... 𝑖 ) ( 𝐹 ‘ 𝑛 ) ) = Σ* 𝑛 ∈ ( 1 ... 𝑖 ) ( 𝑀 ‘ ( ( 𝐹 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) ) ) |
53 |
3
|
ffnd |
⊢ ( 𝜑 → 𝐹 Fn ℕ ) |
54 |
53 4
|
iuninc |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ∪ 𝑛 ∈ ( 1 ... 𝑖 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑖 ) ) |
55 |
54
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 𝑀 ‘ ∪ 𝑛 ∈ ( 1 ... 𝑖 ) ( 𝐹 ‘ 𝑛 ) ) = ( 𝑀 ‘ ( 𝐹 ‘ 𝑖 ) ) ) |
56 |
52 55
|
eqtr3d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → Σ* 𝑛 ∈ ( 1 ... 𝑖 ) ( 𝑀 ‘ ( ( 𝐹 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑀 ‘ ( 𝐹 ‘ 𝑖 ) ) ) |
57 |
56
|
mpteq2dva |
⊢ ( 𝜑 → ( 𝑖 ∈ ℕ ↦ Σ* 𝑛 ∈ ( 1 ... 𝑖 ) ( 𝑀 ‘ ( ( 𝐹 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝑖 ∈ ℕ ↦ ( 𝑀 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) |
58 |
37 57
|
eqtr4d |
⊢ ( 𝜑 → ( 𝑀 ∘ 𝐹 ) = ( 𝑖 ∈ ℕ ↦ Σ* 𝑛 ∈ ( 1 ... 𝑖 ) ( 𝑀 ‘ ( ( 𝐹 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) ) ) ) |
59 |
9
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ 𝑆 ) |
60 |
|
dfiun2g |
⊢ ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ 𝑆 → ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ∪ { 𝑥 ∣ ∃ 𝑛 ∈ ℕ 𝑥 = ( 𝐹 ‘ 𝑛 ) } ) |
61 |
59 60
|
syl |
⊢ ( 𝜑 → ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ∪ { 𝑥 ∣ ∃ 𝑛 ∈ ℕ 𝑥 = ( 𝐹 ‘ 𝑛 ) } ) |
62 |
|
fnrnfv |
⊢ ( 𝐹 Fn ℕ → ran 𝐹 = { 𝑥 ∣ ∃ 𝑛 ∈ ℕ 𝑥 = ( 𝐹 ‘ 𝑛 ) } ) |
63 |
53 62
|
syl |
⊢ ( 𝜑 → ran 𝐹 = { 𝑥 ∣ ∃ 𝑛 ∈ ℕ 𝑥 = ( 𝐹 ‘ 𝑛 ) } ) |
64 |
63
|
unieqd |
⊢ ( 𝜑 → ∪ ran 𝐹 = ∪ { 𝑥 ∣ ∃ 𝑛 ∈ ℕ 𝑥 = ( 𝐹 ‘ 𝑛 ) } ) |
65 |
61 64
|
eqtr4d |
⊢ ( 𝜑 → ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ∪ ran 𝐹 ) |
66 |
65
|
fveq2d |
⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ) = ( 𝑀 ‘ ∪ ran 𝐹 ) ) |
67 |
|
eqidd |
⊢ ( 𝜑 → ℕ = ℕ ) |
68 |
67
|
orcd |
⊢ ( 𝜑 → ( ℕ = ℕ ∨ ℕ = ( 1 ..^ ( 𝑖 + 1 ) ) ) ) |
69 |
38 39 68 2 9
|
measiuns |
⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ) = Σ* 𝑛 ∈ ℕ ( 𝑀 ‘ ( ( 𝐹 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) ) ) |
70 |
66 69
|
eqtr3d |
⊢ ( 𝜑 → ( 𝑀 ‘ ∪ ran 𝐹 ) = Σ* 𝑛 ∈ ℕ ( 𝑀 ‘ ( ( 𝐹 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ) ) ) |
71 |
33 58 70
|
3brtr4d |
⊢ ( 𝜑 → ( 𝑀 ∘ 𝐹 ) ( ⇝𝑡 ‘ 𝐽 ) ( 𝑀 ‘ ∪ ran 𝐹 ) ) |