Step | Hyp | Ref
| Expression |
1 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝑋) → 𝑥 ∈ 𝒫 𝑋) |
2 | | psmeasure.h |
. . . . . . . . 9
⊢ (𝜑 → 𝐻:𝑋⟶(0[,]+∞)) |
3 | 2 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝑋) → 𝐻:𝑋⟶(0[,]+∞)) |
4 | 1 | elpwid 4118 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝑋) → 𝑥 ⊆ 𝑋) |
5 | | fssres 5983 |
. . . . . . . 8
⊢ ((𝐻:𝑋⟶(0[,]+∞) ∧ 𝑥 ⊆ 𝑋) → (𝐻 ↾ 𝑥):𝑥⟶(0[,]+∞)) |
6 | 3, 4, 5 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝑋) → (𝐻 ↾ 𝑥):𝑥⟶(0[,]+∞)) |
7 | 1, 6 | sge0cl 39274 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝑋) →
(Σ^‘(𝐻 ↾ 𝑥)) ∈ (0[,]+∞)) |
8 | | psmeasure.m |
. . . . . 6
⊢ 𝑀 = (𝑥 ∈ 𝒫 𝑋 ↦
(Σ^‘(𝐻 ↾ 𝑥))) |
9 | 7, 8 | fmptd 6292 |
. . . . 5
⊢ (𝜑 → 𝑀:𝒫 𝑋⟶(0[,]+∞)) |
10 | 8, 7 | dmmptd 5937 |
. . . . . 6
⊢ (𝜑 → dom 𝑀 = 𝒫 𝑋) |
11 | 10 | feq2d 5944 |
. . . . 5
⊢ (𝜑 → (𝑀:dom 𝑀⟶(0[,]+∞) ↔ 𝑀:𝒫 𝑋⟶(0[,]+∞))) |
12 | 9, 11 | mpbird 246 |
. . . 4
⊢ (𝜑 → 𝑀:dom 𝑀⟶(0[,]+∞)) |
13 | | psmeasure.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
14 | | pwsal 39211 |
. . . . . 6
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ SAlg) |
15 | 13, 14 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝒫 𝑋 ∈ SAlg) |
16 | 10, 15 | eqeltrd 2688 |
. . . 4
⊢ (𝜑 → dom 𝑀 ∈ SAlg) |
17 | 12, 16 | jca 553 |
. . 3
⊢ (𝜑 → (𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg)) |
18 | 8 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝑀 = (𝑥 ∈ 𝒫 𝑋 ↦
(Σ^‘(𝐻 ↾ 𝑥)))) |
19 | | reseq2 5312 |
. . . . . . 7
⊢ (𝑥 = ∅ → (𝐻 ↾ 𝑥) = (𝐻 ↾ ∅)) |
20 | 19 | fveq2d 6107 |
. . . . . 6
⊢ (𝑥 = ∅ →
(Σ^‘(𝐻 ↾ 𝑥)) =
(Σ^‘(𝐻 ↾ ∅))) |
21 | 20 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 = ∅) →
(Σ^‘(𝐻 ↾ 𝑥)) =
(Σ^‘(𝐻 ↾ ∅))) |
22 | | 0elpw 4760 |
. . . . . 6
⊢ ∅
∈ 𝒫 𝑋 |
23 | 22 | a1i 11 |
. . . . 5
⊢ (𝜑 → ∅ ∈ 𝒫
𝑋) |
24 | | fvex 6113 |
. . . . . 6
⊢
(Σ^‘(𝐻 ↾ ∅)) ∈ V |
25 | 24 | a1i 11 |
. . . . 5
⊢ (𝜑 →
(Σ^‘(𝐻 ↾ ∅)) ∈
V) |
26 | 18, 21, 23, 25 | fvmptd 6197 |
. . . 4
⊢ (𝜑 → (𝑀‘∅) =
(Σ^‘(𝐻 ↾ ∅))) |
27 | | res0 5321 |
. . . . . . 7
⊢ (𝐻 ↾ ∅) =
∅ |
28 | 27 | fveq2i 6106 |
. . . . . 6
⊢
(Σ^‘(𝐻 ↾ ∅)) =
(Σ^‘∅) |
29 | | sge00 39269 |
. . . . . 6
⊢
(Σ^‘∅) = 0 |
30 | 28, 29 | eqtri 2632 |
. . . . 5
⊢
(Σ^‘(𝐻 ↾ ∅)) = 0 |
31 | 30 | a1i 11 |
. . . 4
⊢ (𝜑 →
(Σ^‘(𝐻 ↾ ∅)) = 0) |
32 | 26, 31 | eqtrd 2644 |
. . 3
⊢ (𝜑 → (𝑀‘∅) = 0) |
33 | | simpl 472 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 dom 𝑀) → 𝜑) |
34 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 dom 𝑀) → 𝑦 ∈ 𝒫 dom 𝑀) |
35 | 10 | pweqd 4113 |
. . . . . . . 8
⊢ (𝜑 → 𝒫 dom 𝑀 = 𝒫 𝒫 𝑋) |
36 | 35 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 dom 𝑀) → 𝒫 dom 𝑀 = 𝒫 𝒫 𝑋) |
37 | 34, 36 | eleqtrd 2690 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 dom 𝑀) → 𝑦 ∈ 𝒫 𝒫 𝑋) |
38 | | elpwi 4117 |
. . . . . 6
⊢ (𝑦 ∈ 𝒫 𝒫
𝑋 → 𝑦 ⊆ 𝒫 𝑋) |
39 | 37, 38 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 dom 𝑀) → 𝑦 ⊆ 𝒫 𝑋) |
40 | 13 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ⊆ 𝒫 𝑋) ∧ Disj 𝑤 ∈ 𝑦 𝑤) → 𝑋 ∈ 𝑉) |
41 | 2 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ⊆ 𝒫 𝑋) ∧ Disj 𝑤 ∈ 𝑦 𝑤) → 𝐻:𝑋⟶(0[,]+∞)) |
42 | 9 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ⊆ 𝒫 𝑋) ∧ Disj 𝑤 ∈ 𝑦 𝑤) → 𝑀:𝒫 𝑋⟶(0[,]+∞)) |
43 | | simplr 788 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ⊆ 𝒫 𝑋) ∧ Disj 𝑤 ∈ 𝑦 𝑤) → 𝑦 ⊆ 𝒫 𝑋) |
44 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑧 → 𝑤 = 𝑧) |
45 | 44 | cbvdisjv 4564 |
. . . . . . . . . 10
⊢
(Disj 𝑤
∈ 𝑦 𝑤 ↔ Disj 𝑧 ∈ 𝑦 𝑧) |
46 | 45 | biimpi 205 |
. . . . . . . . 9
⊢
(Disj 𝑤
∈ 𝑦 𝑤 → Disj 𝑧 ∈ 𝑦 𝑧) |
47 | 46 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ⊆ 𝒫 𝑋) ∧ Disj 𝑤 ∈ 𝑦 𝑤) → Disj 𝑧 ∈ 𝑦 𝑧) |
48 | 40, 41, 8, 42, 43, 47 | psmeasurelem 39363 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ⊆ 𝒫 𝑋) ∧ Disj 𝑤 ∈ 𝑦 𝑤) → (𝑀‘∪ 𝑦) =
(Σ^‘(𝑀 ↾ 𝑦))) |
49 | 48 | adantrl 748 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ⊆ 𝒫 𝑋) ∧ (𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤)) → (𝑀‘∪ 𝑦) =
(Σ^‘(𝑀 ↾ 𝑦))) |
50 | 49 | ex 449 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ⊆ 𝒫 𝑋) → ((𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤) → (𝑀‘∪ 𝑦) =
(Σ^‘(𝑀 ↾ 𝑦)))) |
51 | 33, 39, 50 | syl2anc 691 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 dom 𝑀) → ((𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤) → (𝑀‘∪ 𝑦) =
(Σ^‘(𝑀 ↾ 𝑦)))) |
52 | 51 | ralrimiva 2949 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ 𝒫 dom 𝑀((𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤) → (𝑀‘∪ 𝑦) =
(Σ^‘(𝑀 ↾ 𝑦)))) |
53 | 17, 32, 52 | jca31 555 |
. 2
⊢ (𝜑 → (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑦 ∈ 𝒫
dom 𝑀((𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤) → (𝑀‘∪ 𝑦) =
(Σ^‘(𝑀 ↾ 𝑦))))) |
54 | | ismea 39344 |
. 2
⊢ (𝑀 ∈ Meas ↔ (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑦 ∈ 𝒫
dom 𝑀((𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤) → (𝑀‘∪ 𝑦) =
(Σ^‘(𝑀 ↾ 𝑦))))) |
55 | 53, 54 | sylibr 223 |
1
⊢ (𝜑 → 𝑀 ∈ Meas) |