Step |
Hyp |
Ref |
Expression |
1 |
|
meaiuninc.m |
⊢ ( 𝜑 → 𝑀 ∈ Meas ) |
2 |
|
meaiuninc.n |
⊢ ( 𝜑 → 𝑁 ∈ ℤ ) |
3 |
|
meaiuninc.z |
⊢ 𝑍 = ( ℤ≥ ‘ 𝑁 ) |
4 |
|
meaiuninc.e |
⊢ ( 𝜑 → 𝐸 : 𝑍 ⟶ dom 𝑀 ) |
5 |
|
meaiuninc.i |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) ⊆ ( 𝐸 ‘ ( 𝑛 + 1 ) ) ) |
6 |
|
meaiuninc.x |
⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) |
7 |
|
meaiuninc.s |
⊢ 𝑆 = ( 𝑛 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ) |
8 |
|
2fveq3 |
⊢ ( 𝑛 = 𝑚 → ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) = ( 𝑀 ‘ ( 𝐸 ‘ 𝑚 ) ) ) |
9 |
8
|
cbvmptv |
⊢ ( 𝑛 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ) = ( 𝑚 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑚 ) ) ) |
10 |
7 9
|
eqtri |
⊢ 𝑆 = ( 𝑚 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑚 ) ) ) |
11 |
10
|
a1i |
⊢ ( 𝜑 → 𝑆 = ( 𝑚 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑚 ) ) ) ) |
12 |
10 7
|
eqtr3i |
⊢ ( 𝑚 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑚 ) ) ) = ( 𝑛 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ) |
13 |
|
fveq2 |
⊢ ( 𝑘 = 𝑖 → ( 𝐸 ‘ 𝑘 ) = ( 𝐸 ‘ 𝑖 ) ) |
14 |
13
|
cbviunv |
⊢ ∪ 𝑘 ∈ ( 𝑁 ..^ 𝑚 ) ( 𝐸 ‘ 𝑘 ) = ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑚 ) ( 𝐸 ‘ 𝑖 ) |
15 |
14
|
difeq2i |
⊢ ( ( 𝐸 ‘ 𝑚 ) ∖ ∪ 𝑘 ∈ ( 𝑁 ..^ 𝑚 ) ( 𝐸 ‘ 𝑘 ) ) = ( ( 𝐸 ‘ 𝑚 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑚 ) ( 𝐸 ‘ 𝑖 ) ) |
16 |
15
|
mpteq2i |
⊢ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐸 ‘ 𝑚 ) ∖ ∪ 𝑘 ∈ ( 𝑁 ..^ 𝑚 ) ( 𝐸 ‘ 𝑘 ) ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐸 ‘ 𝑚 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑚 ) ( 𝐸 ‘ 𝑖 ) ) ) |
17 |
|
fveq2 |
⊢ ( 𝑚 = 𝑛 → ( 𝐸 ‘ 𝑚 ) = ( 𝐸 ‘ 𝑛 ) ) |
18 |
|
oveq2 |
⊢ ( 𝑚 = 𝑛 → ( 𝑁 ..^ 𝑚 ) = ( 𝑁 ..^ 𝑛 ) ) |
19 |
18
|
iuneq1d |
⊢ ( 𝑚 = 𝑛 → ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑚 ) ( 𝐸 ‘ 𝑖 ) = ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) |
20 |
17 19
|
difeq12d |
⊢ ( 𝑚 = 𝑛 → ( ( 𝐸 ‘ 𝑚 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑚 ) ( 𝐸 ‘ 𝑖 ) ) = ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) ) |
21 |
20
|
cbvmptv |
⊢ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐸 ‘ 𝑚 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑚 ) ( 𝐸 ‘ 𝑖 ) ) ) = ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) ) |
22 |
16 21
|
eqtri |
⊢ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐸 ‘ 𝑚 ) ∖ ∪ 𝑘 ∈ ( 𝑁 ..^ 𝑚 ) ( 𝐸 ‘ 𝑘 ) ) ) = ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) ) |
23 |
1 2 3 4 5 6 12 22
|
meaiuninclem |
⊢ ( 𝜑 → ( 𝑚 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑚 ) ) ) ⇝ ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) |
24 |
11 23
|
eqbrtrd |
⊢ ( 𝜑 → 𝑆 ⇝ ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) |