Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . 5
⊢ (𝑀 ∈ Meas → 𝑀 ∈ Meas) |
2 | | elex 3212 |
. . . . . 6
⊢ (𝑀 ∈ Meas → 𝑀 ∈ V) |
3 | | df-mea 40667 |
. . . . . . . . 9
⊢ Meas =
{𝑧 ∣ (((𝑧:dom 𝑧⟶(0[,]+∞) ∧ dom 𝑧 ∈ SAlg) ∧ (𝑧‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑧((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑧‘∪ 𝑥) =
(Σ^‘(𝑧 ↾ 𝑥))))} |
4 | 3 | eleq2i 2693 |
. . . . . . . 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 5324 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑀 → dom 𝑧 = dom 𝑀) |
8 | 6, 7 | feq12d 6033 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑀 → (𝑧:dom 𝑧⟶(0[,]+∞) ↔ 𝑀:dom 𝑀⟶(0[,]+∞))) |
9 | 7 | eleq1d 2686 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑀 → (dom 𝑧 ∈ SAlg ↔ dom 𝑀 ∈ SAlg)) |
10 | 8, 9 | anbi12d 747 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑀 → ((𝑧:dom 𝑧⟶(0[,]+∞) ∧ dom 𝑧 ∈ SAlg) ↔ (𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg))) |
11 | | fveq1 6190 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑀 → (𝑧‘∅) = (𝑀‘∅)) |
12 | 11 | eqeq1d 2624 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑀 → ((𝑧‘∅) = 0 ↔ (𝑀‘∅) = 0)) |
13 | 10, 12 | anbi12d 747 |
. . . . . . . . 9
⊢ (𝑧 = 𝑀 → (((𝑧:dom 𝑧⟶(0[,]+∞) ∧ dom 𝑧 ∈ SAlg) ∧ (𝑧‘∅) = 0) ↔
((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) =
0))) |
14 | 7 | pweqd 4163 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑀 → 𝒫 dom 𝑧 = 𝒫 dom 𝑀) |
15 | 14 | raleqdv 3144 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑀 → (∀𝑥 ∈ 𝒫 dom 𝑧((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑧‘∪ 𝑥) =
(Σ^‘(𝑧 ↾ 𝑥))) ↔ ∀𝑥 ∈ 𝒫 dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑧‘∪ 𝑥) =
(Σ^‘(𝑧 ↾ 𝑥))))) |
16 | | fveq1 6190 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑀 → (𝑧‘∪ 𝑥) = (𝑀‘∪ 𝑥)) |
17 | | reseq1 5390 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑀 → (𝑧 ↾ 𝑥) = (𝑀 ↾ 𝑥)) |
18 | 17 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑀 →
(Σ^‘(𝑧 ↾ 𝑥)) =
(Σ^‘(𝑀 ↾ 𝑥))) |
19 | 16, 18 | eqeq12d 2637 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑀 → ((𝑧‘∪ 𝑥) =
(Σ^‘(𝑧 ↾ 𝑥)) ↔ (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥)))) |
20 | 19 | imbi2d 330 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑀 → (((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑧‘∪ 𝑥) =
(Σ^‘(𝑧 ↾ 𝑥))) ↔ ((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥))))) |
21 | 20 | ralbidv 2986 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑀 → (∀𝑥 ∈ 𝒫 dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑧‘∪ 𝑥) =
(Σ^‘(𝑧 ↾ 𝑥))) ↔ ∀𝑥 ∈ 𝒫 dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥))))) |
22 | 15, 21 | bitrd 268 |
. . . . . . . . 9
⊢ (𝑧 = 𝑀 → (∀𝑥 ∈ 𝒫 dom 𝑧((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑧‘∪ 𝑥) =
(Σ^‘(𝑧 ↾ 𝑥))) ↔ ∀𝑥 ∈ 𝒫 dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥))))) |
23 | 13, 22 | anbi12d 747 |
. . . . . . . 8
⊢ (𝑧 = 𝑀 → ((((𝑧:dom 𝑧⟶(0[,]+∞) ∧ dom 𝑧 ∈ SAlg) ∧ (𝑧‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑧((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑧‘∪ 𝑥) =
(Σ^‘(𝑧 ↾ 𝑥)))) ↔ (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥)))))) |
24 | 23 | elabg 3351 |
. . . . . . 7
⊢ (𝑀 ∈ V → (𝑀 ∈ {𝑧 ∣ (((𝑧:dom 𝑧⟶(0[,]+∞) ∧ dom 𝑧 ∈ SAlg) ∧ (𝑧‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑧((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑧‘∪ 𝑥) =
(Σ^‘(𝑧 ↾ 𝑥))))} ↔ (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥)))))) |
25 | 5, 24 | bitrd 268 |
. . . . . 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 222 |
. . . 4
⊢ (𝑀 ∈ Meas → (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥))))) |
28 | 27 | simplld 791 |
. . 3
⊢ (𝑀 ∈ Meas → (𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg)) |
29 | 27 | simplrd 793 |
. . 3
⊢ (𝑀 ∈ Meas → (𝑀‘∅) =
0) |
30 | 27 | simprd 479 |
. . 3
⊢ (𝑀 ∈ Meas →
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥)))) |
31 | 28, 29, 30 | jca31 557 |
. 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 6490 |
. . . . 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 762 |
. . 3
⊢ ((((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥)))) → (𝑀 ∈ Meas ↔ (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥)))))) |
36 | 32, 35 | mpbird 247 |
. 2
⊢ ((((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥)))) → 𝑀 ∈ Meas) |
37 | 31, 36 | impbii 199 |
1
⊢ (𝑀 ∈ Meas ↔ (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥))))) |