Step | Hyp | Ref
| Expression |
1 | | iccssxr 12127 |
. . 3
⊢
(0[,]+∞) ⊆ ℝ* |
2 | | omeiunle.o |
. . . 4
⊢ (𝜑 → 𝑂 ∈ OutMeas) |
3 | | omeiunle.x |
. . . 4
⊢ 𝑋 = ∪
dom 𝑂 |
4 | | omeiunle.nph |
. . . . . 6
⊢
Ⅎ𝑛𝜑 |
5 | | omeiunle.e |
. . . . . . . . 9
⊢ (𝜑 → 𝐸:𝑍⟶𝒫 𝑋) |
6 | 5 | ffvelrnda 6267 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ∈ 𝒫 𝑋) |
7 | | elpwi 4117 |
. . . . . . . 8
⊢ ((𝐸‘𝑛) ∈ 𝒫 𝑋 → (𝐸‘𝑛) ⊆ 𝑋) |
8 | 6, 7 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ 𝑋) |
9 | 8 | ex 449 |
. . . . . 6
⊢ (𝜑 → (𝑛 ∈ 𝑍 → (𝐸‘𝑛) ⊆ 𝑋)) |
10 | 4, 9 | ralrimi 2940 |
. . . . 5
⊢ (𝜑 → ∀𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ 𝑋) |
11 | | iunss 4497 |
. . . . 5
⊢ (∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ 𝑋 ↔ ∀𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ 𝑋) |
12 | 10, 11 | sylibr 223 |
. . . 4
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ 𝑋) |
13 | 2, 3, 12 | omecl 39393 |
. . 3
⊢ (𝜑 → (𝑂‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) ∈ (0[,]+∞)) |
14 | 1, 13 | sseldi 3566 |
. 2
⊢ (𝜑 → (𝑂‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) ∈
ℝ*) |
15 | 5 | ffnd 5959 |
. . . . 5
⊢ (𝜑 → 𝐸 Fn 𝑍) |
16 | | omeiunle.z |
. . . . . . 7
⊢ 𝑍 =
(ℤ≥‘𝑁) |
17 | | fvex 6113 |
. . . . . . 7
⊢
(ℤ≥‘𝑁) ∈ V |
18 | 16, 17 | eqeltri 2684 |
. . . . . 6
⊢ 𝑍 ∈ V |
19 | 18 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝑍 ∈ V) |
20 | | fnex 6386 |
. . . . 5
⊢ ((𝐸 Fn 𝑍 ∧ 𝑍 ∈ V) → 𝐸 ∈ V) |
21 | 15, 19, 20 | syl2anc 691 |
. . . 4
⊢ (𝜑 → 𝐸 ∈ V) |
22 | | rnexg 6990 |
. . . 4
⊢ (𝐸 ∈ V → ran 𝐸 ∈ V) |
23 | 21, 22 | syl 17 |
. . 3
⊢ (𝜑 → ran 𝐸 ∈ V) |
24 | 2, 3 | omef 39386 |
. . . 4
⊢ (𝜑 → 𝑂:𝒫 𝑋⟶(0[,]+∞)) |
25 | | frn 5966 |
. . . . 5
⊢ (𝐸:𝑍⟶𝒫 𝑋 → ran 𝐸 ⊆ 𝒫 𝑋) |
26 | 5, 25 | syl 17 |
. . . 4
⊢ (𝜑 → ran 𝐸 ⊆ 𝒫 𝑋) |
27 | 24, 26 | fssresd 5984 |
. . 3
⊢ (𝜑 → (𝑂 ↾ ran 𝐸):ran 𝐸⟶(0[,]+∞)) |
28 | 23, 27 | sge0xrcl 39278 |
. 2
⊢ (𝜑 →
(Σ^‘(𝑂 ↾ ran 𝐸)) ∈
ℝ*) |
29 | 2 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑂 ∈ OutMeas) |
30 | 29, 3, 8 | omecl 39393 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑂‘(𝐸‘𝑛)) ∈ (0[,]+∞)) |
31 | | eqid 2610 |
. . . 4
⊢ (𝑛 ∈ 𝑍 ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ 𝑍 ↦ (𝑂‘(𝐸‘𝑛))) |
32 | 4, 30, 31 | fmptdf 6294 |
. . 3
⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ (𝑂‘(𝐸‘𝑛))):𝑍⟶(0[,]+∞)) |
33 | 19, 32 | sge0xrcl 39278 |
. 2
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑂‘(𝐸‘𝑛)))) ∈
ℝ*) |
34 | | fvex 6113 |
. . . . . . . 8
⊢ (𝐸‘𝑛) ∈ V |
35 | 34 | rgenw 2908 |
. . . . . . 7
⊢
∀𝑛 ∈
𝑍 (𝐸‘𝑛) ∈ V |
36 | | dfiun3g 5299 |
. . . . . . 7
⊢
(∀𝑛 ∈
𝑍 (𝐸‘𝑛) ∈ V → ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) = ∪ ran (𝑛 ∈ 𝑍 ↦ (𝐸‘𝑛))) |
37 | 35, 36 | ax-mp 5 |
. . . . . 6
⊢ ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) = ∪ ran (𝑛 ∈ 𝑍 ↦ (𝐸‘𝑛)) |
38 | 37 | a1i 11 |
. . . . 5
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) = ∪ ran (𝑛 ∈ 𝑍 ↦ (𝐸‘𝑛))) |
39 | 5 | feqmptd 6159 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 = (𝑚 ∈ 𝑍 ↦ (𝐸‘𝑚))) |
40 | | omeiunle.ne |
. . . . . . . . . . 11
⊢
Ⅎ𝑛𝐸 |
41 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛𝑚 |
42 | 40, 41 | nffv 6110 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(𝐸‘𝑚) |
43 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑚(𝐸‘𝑛) |
44 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (𝐸‘𝑚) = (𝐸‘𝑛)) |
45 | 42, 43, 44 | cbvmpt 4677 |
. . . . . . . . 9
⊢ (𝑚 ∈ 𝑍 ↦ (𝐸‘𝑚)) = (𝑛 ∈ 𝑍 ↦ (𝐸‘𝑛)) |
46 | 45 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝑚 ∈ 𝑍 ↦ (𝐸‘𝑚)) = (𝑛 ∈ 𝑍 ↦ (𝐸‘𝑛))) |
47 | 39, 46 | eqtrd 2644 |
. . . . . . 7
⊢ (𝜑 → 𝐸 = (𝑛 ∈ 𝑍 ↦ (𝐸‘𝑛))) |
48 | 47 | rneqd 5274 |
. . . . . 6
⊢ (𝜑 → ran 𝐸 = ran (𝑛 ∈ 𝑍 ↦ (𝐸‘𝑛))) |
49 | 48 | unieqd 4382 |
. . . . 5
⊢ (𝜑 → ∪ ran 𝐸 = ∪ ran (𝑛 ∈ 𝑍 ↦ (𝐸‘𝑛))) |
50 | 38, 49 | eqtr4d 2647 |
. . . 4
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) = ∪ ran 𝐸) |
51 | 50 | fveq2d 6107 |
. . 3
⊢ (𝜑 → (𝑂‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) = (𝑂‘∪ ran
𝐸)) |
52 | | fnrndomg 9239 |
. . . . . 6
⊢ (𝑍 ∈ V → (𝐸 Fn 𝑍 → ran 𝐸 ≼ 𝑍)) |
53 | 19, 15, 52 | sylc 63 |
. . . . 5
⊢ (𝜑 → ran 𝐸 ≼ 𝑍) |
54 | 16 | uzct 38257 |
. . . . . 6
⊢ 𝑍 ≼
ω |
55 | 54 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝑍 ≼ ω) |
56 | | domtr 7895 |
. . . . 5
⊢ ((ran
𝐸 ≼ 𝑍 ∧ 𝑍 ≼ ω) → ran 𝐸 ≼
ω) |
57 | 53, 55, 56 | syl2anc 691 |
. . . 4
⊢ (𝜑 → ran 𝐸 ≼ ω) |
58 | 2, 3, 26, 57 | omeunile 39395 |
. . 3
⊢ (𝜑 → (𝑂‘∪ ran
𝐸) ≤
(Σ^‘(𝑂 ↾ ran 𝐸))) |
59 | 51, 58 | eqbrtrd 4605 |
. 2
⊢ (𝜑 → (𝑂‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) ≤
(Σ^‘(𝑂 ↾ ran 𝐸))) |
60 | | ltweuz 12622 |
. . . . . 6
⊢ < We
(ℤ≥‘𝑁) |
61 | | weeq2 5027 |
. . . . . . 7
⊢ (𝑍 =
(ℤ≥‘𝑁) → ( < We 𝑍 ↔ < We
(ℤ≥‘𝑁))) |
62 | 16, 61 | ax-mp 5 |
. . . . . 6
⊢ ( < We
𝑍 ↔ < We
(ℤ≥‘𝑁)) |
63 | 60, 62 | mpbir 220 |
. . . . 5
⊢ < We
𝑍 |
64 | 63 | a1i 11 |
. . . 4
⊢ (𝜑 → < We 𝑍) |
65 | 19, 24, 5, 64 | sge0resrn 39297 |
. . 3
⊢ (𝜑 →
(Σ^‘(𝑂 ↾ ran 𝐸)) ≤
(Σ^‘(𝑂 ∘ 𝐸))) |
66 | | fcompt 6306 |
. . . . . 6
⊢ ((𝑂:𝒫 𝑋⟶(0[,]+∞) ∧ 𝐸:𝑍⟶𝒫 𝑋) → (𝑂 ∘ 𝐸) = (𝑚 ∈ 𝑍 ↦ (𝑂‘(𝐸‘𝑚)))) |
67 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑛𝑂 |
68 | 67, 42 | nffv 6110 |
. . . . . . . 8
⊢
Ⅎ𝑛(𝑂‘(𝐸‘𝑚)) |
69 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑚(𝑂‘(𝐸‘𝑛)) |
70 | 44 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → (𝑂‘(𝐸‘𝑚)) = (𝑂‘(𝐸‘𝑛))) |
71 | 68, 69, 70 | cbvmpt 4677 |
. . . . . . 7
⊢ (𝑚 ∈ 𝑍 ↦ (𝑂‘(𝐸‘𝑚))) = (𝑛 ∈ 𝑍 ↦ (𝑂‘(𝐸‘𝑛))) |
72 | 71 | a1i 11 |
. . . . . 6
⊢ ((𝑂:𝒫 𝑋⟶(0[,]+∞) ∧ 𝐸:𝑍⟶𝒫 𝑋) → (𝑚 ∈ 𝑍 ↦ (𝑂‘(𝐸‘𝑚))) = (𝑛 ∈ 𝑍 ↦ (𝑂‘(𝐸‘𝑛)))) |
73 | 66, 72 | eqtrd 2644 |
. . . . 5
⊢ ((𝑂:𝒫 𝑋⟶(0[,]+∞) ∧ 𝐸:𝑍⟶𝒫 𝑋) → (𝑂 ∘ 𝐸) = (𝑛 ∈ 𝑍 ↦ (𝑂‘(𝐸‘𝑛)))) |
74 | 24, 5, 73 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (𝑂 ∘ 𝐸) = (𝑛 ∈ 𝑍 ↦ (𝑂‘(𝐸‘𝑛)))) |
75 | 74 | fveq2d 6107 |
. . 3
⊢ (𝜑 →
(Σ^‘(𝑂 ∘ 𝐸)) =
(Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑂‘(𝐸‘𝑛))))) |
76 | 65, 75 | breqtrd 4609 |
. 2
⊢ (𝜑 →
(Σ^‘(𝑂 ↾ ran 𝐸)) ≤
(Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑂‘(𝐸‘𝑛))))) |
77 | 14, 28, 33, 59, 76 | xrletrd 11869 |
1
⊢ (𝜑 → (𝑂‘∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) ≤
(Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑂‘(𝐸‘𝑛))))) |