Step | Hyp | Ref
| Expression |
1 | | meadjiun.1 |
. . . . 5
⊢
Ⅎ𝑘𝜑 |
2 | | meadjiun.b |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑆) |
3 | 2 | ex 449 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ 𝐴 → 𝐵 ∈ 𝑆)) |
4 | 1, 3 | ralrimi 2940 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ 𝑆) |
5 | | dfiun3g 5299 |
. . . 4
⊢
(∀𝑘 ∈
𝐴 𝐵 ∈ 𝑆 → ∪
𝑘 ∈ 𝐴 𝐵 = ∪ ran (𝑘 ∈ 𝐴 ↦ 𝐵)) |
6 | 4, 5 | syl 17 |
. . 3
⊢ (𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 = ∪ ran (𝑘 ∈ 𝐴 ↦ 𝐵)) |
7 | 6 | fveq2d 6107 |
. 2
⊢ (𝜑 → (𝑀‘∪
𝑘 ∈ 𝐴 𝐵) = (𝑀‘∪ ran
(𝑘 ∈ 𝐴 ↦ 𝐵))) |
8 | | meadjiun.m |
. . 3
⊢ (𝜑 → 𝑀 ∈ Meas) |
9 | | meadjiun.s |
. . 3
⊢ 𝑆 = dom 𝑀 |
10 | | eqid 2610 |
. . . . 5
⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵) |
11 | 10 | rnmptss 6299 |
. . . 4
⊢
(∀𝑘 ∈
𝐴 𝐵 ∈ 𝑆 → ran (𝑘 ∈ 𝐴 ↦ 𝐵) ⊆ 𝑆) |
12 | 4, 11 | syl 17 |
. . 3
⊢ (𝜑 → ran (𝑘 ∈ 𝐴 ↦ 𝐵) ⊆ 𝑆) |
13 | | meadjiun.a |
. . . 4
⊢ (𝜑 → 𝐴 ≼ ω) |
14 | | 1stcrestlem 21065 |
. . . 4
⊢ (𝐴 ≼ ω → ran
(𝑘 ∈ 𝐴 ↦ 𝐵) ≼ ω) |
15 | 13, 14 | syl 17 |
. . 3
⊢ (𝜑 → ran (𝑘 ∈ 𝐴 ↦ 𝐵) ≼ ω) |
16 | | meadjiun.dj |
. . . 4
⊢ (𝜑 → Disj 𝑘 ∈ 𝐴 𝐵) |
17 | 10 | disjrnmpt2 38370 |
. . . 4
⊢
(Disj 𝑘
∈ 𝐴 𝐵 → Disj 𝑥 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)𝑥) |
18 | 16, 17 | syl 17 |
. . 3
⊢ (𝜑 → Disj 𝑥 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)𝑥) |
19 | 8, 9, 12, 15, 18 | meadjuni 39350 |
. 2
⊢ (𝜑 → (𝑀‘∪ ran
(𝑘 ∈ 𝐴 ↦ 𝐵)) =
(Σ^‘(𝑀 ↾ ran (𝑘 ∈ 𝐴 ↦ 𝐵)))) |
20 | | reldom 7847 |
. . . . . 6
⊢ Rel
≼ |
21 | | brrelex 5080 |
. . . . . 6
⊢ ((Rel
≼ ∧ 𝐴 ≼
ω) → 𝐴 ∈
V) |
22 | 20, 21 | mpan 702 |
. . . . 5
⊢ (𝐴 ≼ ω → 𝐴 ∈ V) |
23 | 13, 22 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ V) |
24 | 1, 2, 10 | fmptdf 6294 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝑆) |
25 | | fveq2 6103 |
. . . . . 6
⊢ (𝑗 = 𝑖 → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑗) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑖)) |
26 | 25 | neeq1d 2841 |
. . . . 5
⊢ (𝑗 = 𝑖 → (((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑗) ≠ ∅ ↔ ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑖) ≠ ∅)) |
27 | 26 | cbvrabv 3172 |
. . . 4
⊢ {𝑗 ∈ 𝐴 ∣ ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑗) ≠ ∅} = {𝑖 ∈ 𝐴 ∣ ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑖) ≠ ∅} |
28 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → 𝑖 ∈ 𝐴) |
29 | | nfv 1830 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘 𝑖 ∈ 𝐴 |
30 | 1, 29 | nfan 1816 |
. . . . . . . . . 10
⊢
Ⅎ𝑘(𝜑 ∧ 𝑖 ∈ 𝐴) |
31 | | nfcv 2751 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘𝑖 |
32 | 31 | nfcsb1 3514 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘⦋𝑖 / 𝑘⦌𝐵 |
33 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘𝑆 |
34 | 32, 33 | nfel 2763 |
. . . . . . . . . 10
⊢
Ⅎ𝑘⦋𝑖 / 𝑘⦌𝐵 ∈ 𝑆 |
35 | 30, 34 | nfim 1813 |
. . . . . . . . 9
⊢
Ⅎ𝑘((𝜑 ∧ 𝑖 ∈ 𝐴) → ⦋𝑖 / 𝑘⦌𝐵 ∈ 𝑆) |
36 | | eleq1 2676 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑖 → (𝑘 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴)) |
37 | 36 | anbi2d 736 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑖 → ((𝜑 ∧ 𝑘 ∈ 𝐴) ↔ (𝜑 ∧ 𝑖 ∈ 𝐴))) |
38 | | csbeq1a 3508 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑖 → 𝐵 = ⦋𝑖 / 𝑘⦌𝐵) |
39 | 38 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑖 → (𝐵 ∈ 𝑆 ↔ ⦋𝑖 / 𝑘⦌𝐵 ∈ 𝑆)) |
40 | 37, 39 | imbi12d 333 |
. . . . . . . . 9
⊢ (𝑘 = 𝑖 → (((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑆) ↔ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ⦋𝑖 / 𝑘⦌𝐵 ∈ 𝑆))) |
41 | 35, 40, 2 | chvar 2250 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ⦋𝑖 / 𝑘⦌𝐵 ∈ 𝑆) |
42 | 31, 32, 38, 10 | fvmptf 6209 |
. . . . . . . 8
⊢ ((𝑖 ∈ 𝐴 ∧ ⦋𝑖 / 𝑘⦌𝐵 ∈ 𝑆) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑖) = ⦋𝑖 / 𝑘⦌𝐵) |
43 | 28, 41, 42 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑖) = ⦋𝑖 / 𝑘⦌𝐵) |
44 | 43 | disjeq2dv 4558 |
. . . . . 6
⊢ (𝜑 → (Disj 𝑖 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑖) ↔ Disj 𝑖 ∈ 𝐴 ⦋𝑖 / 𝑘⦌𝐵)) |
45 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑖𝐵 |
46 | 45, 32, 38 | cbvdisj 4563 |
. . . . . . . 8
⊢
(Disj 𝑘
∈ 𝐴 𝐵 ↔ Disj 𝑖 ∈ 𝐴 ⦋𝑖 / 𝑘⦌𝐵) |
47 | 46 | bicomi 213 |
. . . . . . 7
⊢
(Disj 𝑖
∈ 𝐴
⦋𝑖 / 𝑘⦌𝐵 ↔ Disj 𝑘 ∈ 𝐴 𝐵) |
48 | 47 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (Disj 𝑖 ∈ 𝐴 ⦋𝑖 / 𝑘⦌𝐵 ↔ Disj 𝑘 ∈ 𝐴 𝐵)) |
49 | 44, 48 | bitrd 267 |
. . . . 5
⊢ (𝜑 → (Disj 𝑖 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑖) ↔ Disj 𝑘 ∈ 𝐴 𝐵)) |
50 | 16, 49 | mpbird 246 |
. . . 4
⊢ (𝜑 → Disj 𝑖 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑖)) |
51 | 8, 9, 23, 24, 27, 50 | meadjiunlem 39358 |
. . 3
⊢ (𝜑 →
(Σ^‘(𝑀 ↾ ran (𝑘 ∈ 𝐴 ↦ 𝐵))) =
(Σ^‘(𝑀 ∘ (𝑘 ∈ 𝐴 ↦ 𝐵)))) |
52 | 45, 32, 38 | cbvmpt 4677 |
. . . . . . 7
⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑖 ∈ 𝐴 ↦ ⦋𝑖 / 𝑘⦌𝐵) |
53 | 52 | coeq2i 5204 |
. . . . . 6
⊢ (𝑀 ∘ (𝑘 ∈ 𝐴 ↦ 𝐵)) = (𝑀 ∘ (𝑖 ∈ 𝐴 ↦ ⦋𝑖 / 𝑘⦌𝐵)) |
54 | 53 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑀 ∘ (𝑘 ∈ 𝐴 ↦ 𝐵)) = (𝑀 ∘ (𝑖 ∈ 𝐴 ↦ ⦋𝑖 / 𝑘⦌𝐵))) |
55 | | eqidd 2611 |
. . . . . 6
⊢ (𝜑 → (𝑖 ∈ 𝐴 ↦ ⦋𝑖 / 𝑘⦌𝐵) = (𝑖 ∈ 𝐴 ↦ ⦋𝑖 / 𝑘⦌𝐵)) |
56 | 8, 9 | meaf 39346 |
. . . . . . 7
⊢ (𝜑 → 𝑀:𝑆⟶(0[,]+∞)) |
57 | 56 | feqmptd 6159 |
. . . . . 6
⊢ (𝜑 → 𝑀 = (𝑦 ∈ 𝑆 ↦ (𝑀‘𝑦))) |
58 | | fveq2 6103 |
. . . . . 6
⊢ (𝑦 = ⦋𝑖 / 𝑘⦌𝐵 → (𝑀‘𝑦) = (𝑀‘⦋𝑖 / 𝑘⦌𝐵)) |
59 | 41, 55, 57, 58 | fmptco 6303 |
. . . . 5
⊢ (𝜑 → (𝑀 ∘ (𝑖 ∈ 𝐴 ↦ ⦋𝑖 / 𝑘⦌𝐵)) = (𝑖 ∈ 𝐴 ↦ (𝑀‘⦋𝑖 / 𝑘⦌𝐵))) |
60 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑖(𝑀‘𝐵) |
61 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑘𝑀 |
62 | 61, 32 | nffv 6110 |
. . . . . . . 8
⊢
Ⅎ𝑘(𝑀‘⦋𝑖 / 𝑘⦌𝐵) |
63 | 38 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑘 = 𝑖 → (𝑀‘𝐵) = (𝑀‘⦋𝑖 / 𝑘⦌𝐵)) |
64 | 60, 62, 63 | cbvmpt 4677 |
. . . . . . 7
⊢ (𝑘 ∈ 𝐴 ↦ (𝑀‘𝐵)) = (𝑖 ∈ 𝐴 ↦ (𝑀‘⦋𝑖 / 𝑘⦌𝐵)) |
65 | 64 | eqcomi 2619 |
. . . . . 6
⊢ (𝑖 ∈ 𝐴 ↦ (𝑀‘⦋𝑖 / 𝑘⦌𝐵)) = (𝑘 ∈ 𝐴 ↦ (𝑀‘𝐵)) |
66 | 65 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑖 ∈ 𝐴 ↦ (𝑀‘⦋𝑖 / 𝑘⦌𝐵)) = (𝑘 ∈ 𝐴 ↦ (𝑀‘𝐵))) |
67 | 54, 59, 66 | 3eqtrd 2648 |
. . . 4
⊢ (𝜑 → (𝑀 ∘ (𝑘 ∈ 𝐴 ↦ 𝐵)) = (𝑘 ∈ 𝐴 ↦ (𝑀‘𝐵))) |
68 | 67 | fveq2d 6107 |
. . 3
⊢ (𝜑 →
(Σ^‘(𝑀 ∘ (𝑘 ∈ 𝐴 ↦ 𝐵))) =
(Σ^‘(𝑘 ∈ 𝐴 ↦ (𝑀‘𝐵)))) |
69 | 51, 68 | eqtrd 2644 |
. 2
⊢ (𝜑 →
(Σ^‘(𝑀 ↾ ran (𝑘 ∈ 𝐴 ↦ 𝐵))) =
(Σ^‘(𝑘 ∈ 𝐴 ↦ (𝑀‘𝐵)))) |
70 | 7, 19, 69 | 3eqtrd 2648 |
1
⊢ (𝜑 → (𝑀‘∪
𝑘 ∈ 𝐴 𝐵) =
(Σ^‘(𝑘 ∈ 𝐴 ↦ (𝑀‘𝐵)))) |