Step | Hyp | Ref
| Expression |
1 | | simpr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝑋) → 𝑥 ∈ 𝒫 𝑋) |
2 | | psmeasure.h |
. . . . . . . . 9
⊢ (𝜑 → 𝐻:𝑋⟶(0[,]+∞)) |
3 | 2 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝑋) → 𝐻:𝑋⟶(0[,]+∞)) |
4 | 1 | elpwid 4550 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝑋) → 𝑥 ⊆ 𝑋) |
5 | | fssres 6638 |
. . . . . . . 8
⊢ ((𝐻:𝑋⟶(0[,]+∞) ∧ 𝑥 ⊆ 𝑋) → (𝐻 ↾ 𝑥):𝑥⟶(0[,]+∞)) |
6 | 3, 4, 5 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝑋) → (𝐻 ↾ 𝑥):𝑥⟶(0[,]+∞)) |
7 | 1, 6 | sge0cl 43890 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝑋) →
(Σ^‘(𝐻 ↾ 𝑥)) ∈ (0[,]+∞)) |
8 | | psmeasure.m |
. . . . . 6
⊢ 𝑀 = (𝑥 ∈ 𝒫 𝑋 ↦
(Σ^‘(𝐻 ↾ 𝑥))) |
9 | 7, 8 | fmptd 6985 |
. . . . 5
⊢ (𝜑 → 𝑀:𝒫 𝑋⟶(0[,]+∞)) |
10 | 8, 7 | dmmptd 6576 |
. . . . . 6
⊢ (𝜑 → dom 𝑀 = 𝒫 𝑋) |
11 | 10 | feq2d 6584 |
. . . . 5
⊢ (𝜑 → (𝑀:dom 𝑀⟶(0[,]+∞) ↔ 𝑀:𝒫 𝑋⟶(0[,]+∞))) |
12 | 9, 11 | mpbird 256 |
. . . 4
⊢ (𝜑 → 𝑀:dom 𝑀⟶(0[,]+∞)) |
13 | | psmeasure.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
14 | | pwsal 43827 |
. . . . . 6
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ SAlg) |
15 | 13, 14 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝒫 𝑋 ∈ SAlg) |
16 | 10, 15 | eqeltrd 2841 |
. . . 4
⊢ (𝜑 → dom 𝑀 ∈ SAlg) |
17 | 12, 16 | jca 512 |
. . 3
⊢ (𝜑 → (𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg)) |
18 | | reseq2 5885 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝐻 ↾ 𝑥) = (𝐻 ↾ ∅)) |
19 | 18 | fveq2d 6775 |
. . . . 5
⊢ (𝑥 = ∅ →
(Σ^‘(𝐻 ↾ 𝑥)) =
(Σ^‘(𝐻 ↾ ∅))) |
20 | | 0elpw 5282 |
. . . . . 6
⊢ ∅
∈ 𝒫 𝑋 |
21 | 20 | a1i 11 |
. . . . 5
⊢ (𝜑 → ∅ ∈ 𝒫
𝑋) |
22 | | fvexd 6786 |
. . . . 5
⊢ (𝜑 →
(Σ^‘(𝐻 ↾ ∅)) ∈
V) |
23 | 8, 19, 21, 22 | fvmptd3 6895 |
. . . 4
⊢ (𝜑 → (𝑀‘∅) =
(Σ^‘(𝐻 ↾ ∅))) |
24 | | res0 5894 |
. . . . . . 7
⊢ (𝐻 ↾ ∅) =
∅ |
25 | 24 | fveq2i 6774 |
. . . . . 6
⊢
(Σ^‘(𝐻 ↾ ∅)) =
(Σ^‘∅) |
26 | | sge00 43885 |
. . . . . 6
⊢
(Σ^‘∅) = 0 |
27 | 25, 26 | eqtri 2768 |
. . . . 5
⊢
(Σ^‘(𝐻 ↾ ∅)) = 0 |
28 | 27 | a1i 11 |
. . . 4
⊢ (𝜑 →
(Σ^‘(𝐻 ↾ ∅)) = 0) |
29 | 23, 28 | eqtrd 2780 |
. . 3
⊢ (𝜑 → (𝑀‘∅) = 0) |
30 | | simpl 483 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 dom 𝑀) → 𝜑) |
31 | | simpr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 dom 𝑀) → 𝑦 ∈ 𝒫 dom 𝑀) |
32 | 10 | pweqd 4558 |
. . . . . . . 8
⊢ (𝜑 → 𝒫 dom 𝑀 = 𝒫 𝒫 𝑋) |
33 | 32 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 dom 𝑀) → 𝒫 dom 𝑀 = 𝒫 𝒫 𝑋) |
34 | 31, 33 | eleqtrd 2843 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 dom 𝑀) → 𝑦 ∈ 𝒫 𝒫 𝑋) |
35 | | elpwi 4548 |
. . . . . 6
⊢ (𝑦 ∈ 𝒫 𝒫
𝑋 → 𝑦 ⊆ 𝒫 𝑋) |
36 | 34, 35 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 dom 𝑀) → 𝑦 ⊆ 𝒫 𝑋) |
37 | 13 | ad2antrr 723 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ⊆ 𝒫 𝑋) ∧ Disj 𝑤 ∈ 𝑦 𝑤) → 𝑋 ∈ 𝑉) |
38 | 2 | ad2antrr 723 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ⊆ 𝒫 𝑋) ∧ Disj 𝑤 ∈ 𝑦 𝑤) → 𝐻:𝑋⟶(0[,]+∞)) |
39 | 9 | ad2antrr 723 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ⊆ 𝒫 𝑋) ∧ Disj 𝑤 ∈ 𝑦 𝑤) → 𝑀:𝒫 𝑋⟶(0[,]+∞)) |
40 | | simplr 766 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ⊆ 𝒫 𝑋) ∧ Disj 𝑤 ∈ 𝑦 𝑤) → 𝑦 ⊆ 𝒫 𝑋) |
41 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑧 → 𝑤 = 𝑧) |
42 | 41 | cbvdisjv 5055 |
. . . . . . . . . 10
⊢
(Disj 𝑤
∈ 𝑦 𝑤 ↔ Disj 𝑧 ∈ 𝑦 𝑧) |
43 | 42 | biimpi 215 |
. . . . . . . . 9
⊢
(Disj 𝑤
∈ 𝑦 𝑤 → Disj 𝑧 ∈ 𝑦 𝑧) |
44 | 43 | adantl 482 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ⊆ 𝒫 𝑋) ∧ Disj 𝑤 ∈ 𝑦 𝑤) → Disj 𝑧 ∈ 𝑦 𝑧) |
45 | 37, 38, 8, 39, 40, 44 | psmeasurelem 43979 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ⊆ 𝒫 𝑋) ∧ Disj 𝑤 ∈ 𝑦 𝑤) → (𝑀‘∪ 𝑦) =
(Σ^‘(𝑀 ↾ 𝑦))) |
46 | 45 | adantrl 713 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ⊆ 𝒫 𝑋) ∧ (𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤)) → (𝑀‘∪ 𝑦) =
(Σ^‘(𝑀 ↾ 𝑦))) |
47 | 46 | ex 413 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ⊆ 𝒫 𝑋) → ((𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤) → (𝑀‘∪ 𝑦) =
(Σ^‘(𝑀 ↾ 𝑦)))) |
48 | 30, 36, 47 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 dom 𝑀) → ((𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤) → (𝑀‘∪ 𝑦) =
(Σ^‘(𝑀 ↾ 𝑦)))) |
49 | 48 | ralrimiva 3110 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ 𝒫 dom 𝑀((𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤) → (𝑀‘∪ 𝑦) =
(Σ^‘(𝑀 ↾ 𝑦)))) |
50 | 17, 29, 49 | jca31 515 |
. 2
⊢ (𝜑 → (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑦 ∈ 𝒫
dom 𝑀((𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤) → (𝑀‘∪ 𝑦) =
(Σ^‘(𝑀 ↾ 𝑦))))) |
51 | | ismea 43960 |
. 2
⊢ (𝑀 ∈ Meas ↔ (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑦 ∈ 𝒫
dom 𝑀((𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤) → (𝑀‘∪ 𝑦) =
(Σ^‘(𝑀 ↾ 𝑦))))) |
52 | 50, 51 | sylibr 233 |
1
⊢ (𝜑 → 𝑀 ∈ Meas) |