Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . 5
⊢ (𝑀 ∈ Meas → 𝑀 ∈ Meas) |
2 | | elex 3185 |
. . . . . 6
⊢ (𝑀 ∈ Meas → 𝑀 ∈ V) |
3 | | df-mea 39343 |
. . . . . . . . 9
⊢ Meas =
{𝑧 ∣ (((𝑧:dom 𝑧⟶(0[,]+∞) ∧ dom 𝑧 ∈ SAlg) ∧ (𝑧‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑧((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑧‘∪ 𝑥) =
(Σ^‘(𝑧 ↾ 𝑥))))} |
4 | 3 | eleq2i 2680 |
. . . . . . . 8
⊢ (𝑀 ∈ Meas ↔ 𝑀 ∈ {𝑧 ∣ (((𝑧:dom 𝑧⟶(0[,]+∞) ∧ dom 𝑧 ∈ SAlg) ∧ (𝑧‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑧((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑧‘∪ 𝑥) =
(Σ^‘(𝑧 ↾ 𝑥))))}) |
5 | 4 | a1i 11 |
. . . . . . 7
⊢ (𝑀 ∈ V → (𝑀 ∈ Meas ↔ 𝑀 ∈ {𝑧 ∣ (((𝑧:dom 𝑧⟶(0[,]+∞) ∧ dom 𝑧 ∈ SAlg) ∧ (𝑧‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑧((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑧‘∪ 𝑥) =
(Σ^‘(𝑧 ↾ 𝑥))))})) |
6 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑀 → 𝑧 = 𝑀) |
7 | | dmeq 5246 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑀 → dom 𝑧 = dom 𝑀) |
8 | 6, 7 | feq12d 5946 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑀 → (𝑧:dom 𝑧⟶(0[,]+∞) ↔ 𝑀:dom 𝑀⟶(0[,]+∞))) |
9 | 7 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑀 → (dom 𝑧 ∈ SAlg ↔ dom 𝑀 ∈ SAlg)) |
10 | 8, 9 | anbi12d 743 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑀 → ((𝑧:dom 𝑧⟶(0[,]+∞) ∧ dom 𝑧 ∈ SAlg) ↔ (𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg))) |
11 | | fveq1 6102 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑀 → (𝑧‘∅) = (𝑀‘∅)) |
12 | 11 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑀 → ((𝑧‘∅) = 0 ↔ (𝑀‘∅) = 0)) |
13 | 10, 12 | anbi12d 743 |
. . . . . . . . 9
⊢ (𝑧 = 𝑀 → (((𝑧:dom 𝑧⟶(0[,]+∞) ∧ dom 𝑧 ∈ SAlg) ∧ (𝑧‘∅) = 0) ↔
((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) =
0))) |
14 | 7 | pweqd 4113 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑀 → 𝒫 dom 𝑧 = 𝒫 dom 𝑀) |
15 | 14 | raleqdv 3121 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑀 → (∀𝑥 ∈ 𝒫 dom 𝑧((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑧‘∪ 𝑥) =
(Σ^‘(𝑧 ↾ 𝑥))) ↔ ∀𝑥 ∈ 𝒫 dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑧‘∪ 𝑥) =
(Σ^‘(𝑧 ↾ 𝑥))))) |
16 | | fveq1 6102 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑀 → (𝑧‘∪ 𝑥) = (𝑀‘∪ 𝑥)) |
17 | | reseq1 5311 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑀 → (𝑧 ↾ 𝑥) = (𝑀 ↾ 𝑥)) |
18 | 17 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑀 →
(Σ^‘(𝑧 ↾ 𝑥)) =
(Σ^‘(𝑀 ↾ 𝑥))) |
19 | 16, 18 | eqeq12d 2625 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑀 → ((𝑧‘∪ 𝑥) =
(Σ^‘(𝑧 ↾ 𝑥)) ↔ (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥)))) |
20 | 19 | imbi2d 329 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑀 → (((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑧‘∪ 𝑥) =
(Σ^‘(𝑧 ↾ 𝑥))) ↔ ((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥))))) |
21 | 20 | ralbidv 2969 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑀 → (∀𝑥 ∈ 𝒫 dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑧‘∪ 𝑥) =
(Σ^‘(𝑧 ↾ 𝑥))) ↔ ∀𝑥 ∈ 𝒫 dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥))))) |
22 | 15, 21 | bitrd 267 |
. . . . . . . . 9
⊢ (𝑧 = 𝑀 → (∀𝑥 ∈ 𝒫 dom 𝑧((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑧‘∪ 𝑥) =
(Σ^‘(𝑧 ↾ 𝑥))) ↔ ∀𝑥 ∈ 𝒫 dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥))))) |
23 | 13, 22 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑧 = 𝑀 → ((((𝑧:dom 𝑧⟶(0[,]+∞) ∧ dom 𝑧 ∈ SAlg) ∧ (𝑧‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑧((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑧‘∪ 𝑥) =
(Σ^‘(𝑧 ↾ 𝑥)))) ↔ (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥)))))) |
24 | 23 | elabg 3320 |
. . . . . . 7
⊢ (𝑀 ∈ V → (𝑀 ∈ {𝑧 ∣ (((𝑧:dom 𝑧⟶(0[,]+∞) ∧ dom 𝑧 ∈ SAlg) ∧ (𝑧‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑧((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑧‘∪ 𝑥) =
(Σ^‘(𝑧 ↾ 𝑥))))} ↔ (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥)))))) |
25 | 5, 24 | bitrd 267 |
. . . . . 6
⊢ (𝑀 ∈ V → (𝑀 ∈ Meas ↔ (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥)))))) |
26 | 2, 25 | syl 17 |
. . . . 5
⊢ (𝑀 ∈ Meas → (𝑀 ∈ Meas ↔ (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥)))))) |
27 | 1, 26 | mpbid 221 |
. . . 4
⊢ (𝑀 ∈ Meas → (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥))))) |
28 | 27 | simplld 787 |
. . 3
⊢ (𝑀 ∈ Meas → (𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg)) |
29 | 27 | simplrd 789 |
. . 3
⊢ (𝑀 ∈ Meas → (𝑀‘∅) =
0) |
30 | 27 | simprd 478 |
. . 3
⊢ (𝑀 ∈ Meas →
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥)))) |
31 | 28, 29, 30 | jca31 555 |
. 2
⊢ (𝑀 ∈ Meas → (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥))))) |
32 | | id 22 |
. . 3
⊢ ((((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥)))) → (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥))))) |
33 | | fex 6394 |
. . . . 5
⊢ ((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) → 𝑀 ∈ V) |
34 | 33, 25 | syl 17 |
. . . 4
⊢ ((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) → (𝑀 ∈ Meas ↔ (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥)))))) |
35 | 34 | ad2antrr 758 |
. . 3
⊢ ((((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥)))) → (𝑀 ∈ Meas ↔ (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥)))))) |
36 | 32, 35 | mpbird 246 |
. 2
⊢ ((((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥)))) → 𝑀 ∈ Meas) |
37 | 31, 36 | impbii 198 |
1
⊢ (𝑀 ∈ Meas ↔ (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥))))) |