| Step | Hyp | Ref
| Expression |
| 1 | | id 22 |
. 2
⊢ (𝑀 ∈ Meas → 𝑀 ∈ Meas) |
| 2 | | fex 7246 |
. . . . 5
⊢ ((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) → 𝑀 ∈ V) |
| 3 | | id 22 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑀 → 𝑧 = 𝑀) |
| 4 | | dmeq 5914 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑀 → dom 𝑧 = dom 𝑀) |
| 5 | 3, 4 | feq12d 6724 |
. . . . . . . . 9
⊢ (𝑧 = 𝑀 → (𝑧:dom 𝑧⟶(0[,]+∞) ↔ 𝑀:dom 𝑀⟶(0[,]+∞))) |
| 6 | 4 | eleq1d 2826 |
. . . . . . . . 9
⊢ (𝑧 = 𝑀 → (dom 𝑧 ∈ SAlg ↔ dom 𝑀 ∈ SAlg)) |
| 7 | 5, 6 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑧 = 𝑀 → ((𝑧:dom 𝑧⟶(0[,]+∞) ∧ dom 𝑧 ∈ SAlg) ↔ (𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg))) |
| 8 | | fveq1 6905 |
. . . . . . . . 9
⊢ (𝑧 = 𝑀 → (𝑧‘∅) = (𝑀‘∅)) |
| 9 | 8 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑧 = 𝑀 → ((𝑧‘∅) = 0 ↔ (𝑀‘∅) = 0)) |
| 10 | 7, 9 | anbi12d 632 |
. . . . . . 7
⊢ (𝑧 = 𝑀 → (((𝑧:dom 𝑧⟶(0[,]+∞) ∧ dom 𝑧 ∈ SAlg) ∧ (𝑧‘∅) = 0) ↔
((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) =
0))) |
| 11 | 4 | pweqd 4617 |
. . . . . . . 8
⊢ (𝑧 = 𝑀 → 𝒫 dom 𝑧 = 𝒫 dom 𝑀) |
| 12 | | fveq1 6905 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑀 → (𝑧‘∪ 𝑥) = (𝑀‘∪ 𝑥)) |
| 13 | | reseq1 5991 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑀 → (𝑧 ↾ 𝑥) = (𝑀 ↾ 𝑥)) |
| 14 | 13 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑀 →
(Σ^‘(𝑧 ↾ 𝑥)) =
(Σ^‘(𝑀 ↾ 𝑥))) |
| 15 | 12, 14 | eqeq12d 2753 |
. . . . . . . . 9
⊢ (𝑧 = 𝑀 → ((𝑧‘∪ 𝑥) =
(Σ^‘(𝑧 ↾ 𝑥)) ↔ (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥)))) |
| 16 | 15 | imbi2d 340 |
. . . . . . . 8
⊢ (𝑧 = 𝑀 → (((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑧‘∪ 𝑥) =
(Σ^‘(𝑧 ↾ 𝑥))) ↔ ((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥))))) |
| 17 | 11, 16 | raleqbidv 3346 |
. . . . . . 7
⊢ (𝑧 = 𝑀 → (∀𝑥 ∈ 𝒫 dom 𝑧((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑧‘∪ 𝑥) =
(Σ^‘(𝑧 ↾ 𝑥))) ↔ ∀𝑥 ∈ 𝒫 dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥))))) |
| 18 | 10, 17 | anbi12d 632 |
. . . . . 6
⊢ (𝑧 = 𝑀 → ((((𝑧:dom 𝑧⟶(0[,]+∞) ∧ dom 𝑧 ∈ SAlg) ∧ (𝑧‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑧((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑧‘∪ 𝑥) =
(Σ^‘(𝑧 ↾ 𝑥)))) ↔ (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥)))))) |
| 19 | | df-mea 46465 |
. . . . . 6
⊢ Meas =
{𝑧 ∣ (((𝑧:dom 𝑧⟶(0[,]+∞) ∧ dom 𝑧 ∈ SAlg) ∧ (𝑧‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑧((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑧‘∪ 𝑥) =
(Σ^‘(𝑧 ↾ 𝑥))))} |
| 20 | 18, 19 | elab2g 3680 |
. . . . 5
⊢ (𝑀 ∈ V → (𝑀 ∈ Meas ↔ (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥)))))) |
| 21 | 2, 20 | syl 17 |
. . . 4
⊢ ((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) → (𝑀 ∈ Meas ↔ (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥)))))) |
| 22 | 21 | ad2antrr 726 |
. . 3
⊢ ((((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥)))) → (𝑀 ∈ Meas ↔ (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥)))))) |
| 23 | 22 | ibir 268 |
. 2
⊢ ((((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥)))) → 𝑀 ∈ Meas) |
| 24 | 18, 19 | elab2g 3680 |
. 2
⊢ (𝑀 ∈ Meas → (𝑀 ∈ Meas ↔ (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥)))))) |
| 25 | 1, 23, 24 | pm5.21nii 378 |
1
⊢ (𝑀 ∈ Meas ↔ (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧
∀𝑥 ∈ 𝒫
dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) =
(Σ^‘(𝑀 ↾ 𝑥))))) |