Step |
Hyp |
Ref |
Expression |
1 |
|
meaiininc2.f |
⊢ Ⅎ 𝑛 𝜑 |
2 |
|
meaiininc2.p |
⊢ Ⅎ 𝑘 𝜑 |
3 |
|
meaiininc2.m |
⊢ ( 𝜑 → 𝑀 ∈ Meas ) |
4 |
|
meaiininc2.n |
⊢ ( 𝜑 → 𝑁 ∈ ℤ ) |
5 |
|
meaiininc2.z |
⊢ 𝑍 = ( ℤ≥ ‘ 𝑁 ) |
6 |
|
meaiininc2.e |
⊢ ( 𝜑 → 𝐸 : 𝑍 ⟶ dom 𝑀 ) |
7 |
|
meaiininc2.i |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ ( 𝑛 + 1 ) ) ⊆ ( 𝐸 ‘ 𝑛 ) ) |
8 |
|
meaiininc2.k |
⊢ ( 𝜑 → ∃ 𝑘 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑘 ) ) ∈ ℝ ) |
9 |
|
meaiininc2.s |
⊢ 𝑆 = ( 𝑛 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ) |
10 |
|
nfv |
⊢ Ⅎ 𝑘 𝑆 ⇝ ( 𝑀 ‘ ∩ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) |
11 |
|
nfv |
⊢ Ⅎ 𝑛 𝑘 ∈ 𝑍 |
12 |
|
nfv |
⊢ Ⅎ 𝑛 ( 𝑀 ‘ ( 𝐸 ‘ 𝑘 ) ) ∈ ℝ |
13 |
1 11 12
|
nf3an |
⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( 𝑀 ‘ ( 𝐸 ‘ 𝑘 ) ) ∈ ℝ ) |
14 |
3
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( 𝑀 ‘ ( 𝐸 ‘ 𝑘 ) ) ∈ ℝ ) → 𝑀 ∈ Meas ) |
15 |
4
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( 𝑀 ‘ ( 𝐸 ‘ 𝑘 ) ) ∈ ℝ ) → 𝑁 ∈ ℤ ) |
16 |
6
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( 𝑀 ‘ ( 𝐸 ‘ 𝑘 ) ) ∈ ℝ ) → 𝐸 : 𝑍 ⟶ dom 𝑀 ) |
17 |
7
|
3ad2antl1 |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( 𝑀 ‘ ( 𝐸 ‘ 𝑘 ) ) ∈ ℝ ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ ( 𝑛 + 1 ) ) ⊆ ( 𝐸 ‘ 𝑛 ) ) |
18 |
|
id |
⊢ ( 𝑘 ∈ 𝑍 → 𝑘 ∈ 𝑍 ) |
19 |
18 5
|
eleqtrdi |
⊢ ( 𝑘 ∈ 𝑍 → 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) |
20 |
19
|
3ad2ant2 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( 𝑀 ‘ ( 𝐸 ‘ 𝑘 ) ) ∈ ℝ ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) |
21 |
|
simp3 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( 𝑀 ‘ ( 𝐸 ‘ 𝑘 ) ) ∈ ℝ ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑘 ) ) ∈ ℝ ) |
22 |
13 14 15 5 16 17 20 21 9
|
meaiininc |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( 𝑀 ‘ ( 𝐸 ‘ 𝑘 ) ) ∈ ℝ ) → 𝑆 ⇝ ( 𝑀 ‘ ∩ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) |
23 |
22
|
3exp |
⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 → ( ( 𝑀 ‘ ( 𝐸 ‘ 𝑘 ) ) ∈ ℝ → 𝑆 ⇝ ( 𝑀 ‘ ∩ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) ) |
24 |
2 10 23
|
rexlimd |
⊢ ( 𝜑 → ( ∃ 𝑘 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑘 ) ) ∈ ℝ → 𝑆 ⇝ ( 𝑀 ‘ ∩ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) |
25 |
8 24
|
mpd |
⊢ ( 𝜑 → 𝑆 ⇝ ( 𝑀 ‘ ∩ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) |