Step | Hyp | Ref
| Expression |
1 | | meaiunlelem.1 |
. . . . . . 7
⊢
Ⅎ𝑛𝜑 |
2 | | meaiunlelem.z |
. . . . . . 7
⊢ 𝑍 =
(ℤ≥‘𝑁) |
3 | | meaiunlelem.e |
. . . . . . 7
⊢ (𝜑 → 𝐸:𝑍⟶𝑆) |
4 | | meaiunlelem.f |
. . . . . . 7
⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
5 | 1, 2, 3, 4 | iundjiun 40677 |
. . . . . 6
⊢ (𝜑 → ((∀𝑥 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑥)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑥)(𝐸‘𝑛) ∧ ∪
𝑛 ∈ 𝑍 (𝐹‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ∧ Disj 𝑛 ∈ 𝑍 (𝐹‘𝑛))) |
6 | 5 | simplrd 793 |
. . . . 5
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) |
7 | 6 | eqcomd 2628 |
. . . 4
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛)) |
8 | 7 | fveq2d 6195 |
. . 3
⊢ (𝜑 → (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) = (𝑀‘∪
𝑛 ∈ 𝑍 (𝐹‘𝑛))) |
9 | | meaiunlelem.m |
. . . 4
⊢ (𝜑 → 𝑀 ∈ Meas) |
10 | | meaiunlelem.s |
. . . 4
⊢ 𝑆 = dom 𝑀 |
11 | 9, 10 | dmmeasal 40669 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ SAlg) |
12 | 11 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑆 ∈ SAlg) |
13 | 3 | ffvelrnda 6359 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ∈ 𝑆) |
14 | | fzofi 12773 |
. . . . . . . . . . 11
⊢ (𝑁..^𝑛) ∈ Fin |
15 | | isfinite 8549 |
. . . . . . . . . . . . 13
⊢ ((𝑁..^𝑛) ∈ Fin ↔ (𝑁..^𝑛) ≺ ω) |
16 | 15 | biimpi 206 |
. . . . . . . . . . . 12
⊢ ((𝑁..^𝑛) ∈ Fin → (𝑁..^𝑛) ≺ ω) |
17 | | sdomdom 7983 |
. . . . . . . . . . . 12
⊢ ((𝑁..^𝑛) ≺ ω → (𝑁..^𝑛) ≼ ω) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁..^𝑛) ∈ Fin → (𝑁..^𝑛) ≼ ω) |
19 | 14, 18 | ax-mp 5 |
. . . . . . . . . 10
⊢ (𝑁..^𝑛) ≼ ω |
20 | 19 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁..^𝑛) ≼ ω) |
21 | 3 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝐸:𝑍⟶𝑆) |
22 | | elfzouz 12474 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (𝑁..^𝑛) → 𝑖 ∈ (ℤ≥‘𝑁)) |
23 | 2 | eqcomi 2631 |
. . . . . . . . . . . 12
⊢
(ℤ≥‘𝑁) = 𝑍 |
24 | 22, 23 | syl6eleq 2711 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (𝑁..^𝑛) → 𝑖 ∈ 𝑍) |
25 | 24 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ∈ 𝑍) |
26 | 21, 25 | ffvelrnd 6360 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝐸‘𝑖) ∈ 𝑆) |
27 | 11, 20, 26 | saliuncl 40542 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖) ∈ 𝑆) |
28 | 27 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖) ∈ 𝑆) |
29 | | saldifcl2 40546 |
. . . . . . 7
⊢ ((𝑆 ∈ SAlg ∧ (𝐸‘𝑛) ∈ 𝑆 ∧ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖) ∈ 𝑆) → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ 𝑆) |
30 | 12, 13, 28, 29 | syl3anc 1326 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ 𝑆) |
31 | 1, 30, 4 | fmptdf 6387 |
. . . . 5
⊢ (𝜑 → 𝐹:𝑍⟶𝑆) |
32 | 31 | ffvelrnda 6359 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ 𝑆) |
33 | | eqid 2622 |
. . . . . . 7
⊢
(ℤ≥‘𝑁) = (ℤ≥‘𝑁) |
34 | 33 | uzct 39232 |
. . . . . 6
⊢
(ℤ≥‘𝑁) ≼ ω |
35 | 2, 34 | eqbrtri 4674 |
. . . . 5
⊢ 𝑍 ≼
ω |
36 | 35 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑍 ≼ ω) |
37 | 5 | simprd 479 |
. . . 4
⊢ (𝜑 → Disj 𝑛 ∈ 𝑍 (𝐹‘𝑛)) |
38 | 1, 9, 10, 32, 36, 37 | meadjiun 40683 |
. . 3
⊢ (𝜑 → (𝑀‘∪
𝑛 ∈ 𝑍 (𝐹‘𝑛)) =
(Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛))))) |
39 | | eqidd 2623 |
. . 3
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛)))) =
(Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛))))) |
40 | 8, 38, 39 | 3eqtrd 2660 |
. 2
⊢ (𝜑 → (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) =
(Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛))))) |
41 | | fvex 6201 |
. . . . 5
⊢
(ℤ≥‘𝑁) ∈ V |
42 | 2, 41 | eqeltri 2697 |
. . . 4
⊢ 𝑍 ∈ V |
43 | 42 | a1i 11 |
. . 3
⊢ (𝜑 → 𝑍 ∈ V) |
44 | 9 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑀 ∈ Meas) |
45 | 44, 10, 32 | meacl 40675 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) ∈ (0[,]+∞)) |
46 | 44, 10, 13 | meacl 40675 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ∈ (0[,]+∞)) |
47 | | simpr 477 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ 𝑍) |
48 | | difexg 4808 |
. . . . . . 7
⊢ ((𝐸‘𝑛) ∈ 𝑆 → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ V) |
49 | 13, 48 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ V) |
50 | 4 | fvmpt2 6291 |
. . . . . 6
⊢ ((𝑛 ∈ 𝑍 ∧ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ V) → (𝐹‘𝑛) = ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
51 | 47, 49, 50 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
52 | | difssd 3738 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ⊆ (𝐸‘𝑛)) |
53 | 51, 52 | eqsstrd 3639 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ⊆ (𝐸‘𝑛)) |
54 | 44, 10, 32, 13, 53 | meassle 40680 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) ≤ (𝑀‘(𝐸‘𝑛))) |
55 | 1, 43, 45, 46, 54 | sge0lempt 40627 |
. 2
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛)))) ≤
(Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))))) |
56 | 40, 55 | eqbrtrd 4675 |
1
⊢ (𝜑 → (𝑀‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) ≤
(Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))))) |