Step |
Hyp |
Ref |
Expression |
1 |
|
isrnmeas |
⊢ ( 𝑀 ∈ ∪ ran measures → ( dom 𝑀 ∈ ∪ ran sigAlgebra ∧ ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑀 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 dom 𝑀 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) ) ) ) ) |
2 |
1
|
simprd |
⊢ ( 𝑀 ∈ ∪ ran measures → ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑀 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 dom 𝑀 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) ) ) ) |
3 |
|
dmmeas |
⊢ ( 𝑀 ∈ ∪ ran measures → dom 𝑀 ∈ ∪ ran sigAlgebra ) |
4 |
|
ismeas |
⊢ ( dom 𝑀 ∈ ∪ ran sigAlgebra → ( 𝑀 ∈ ( measures ‘ dom 𝑀 ) ↔ ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑀 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 dom 𝑀 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) ) ) ) ) |
5 |
3 4
|
syl |
⊢ ( 𝑀 ∈ ∪ ran measures → ( 𝑀 ∈ ( measures ‘ dom 𝑀 ) ↔ ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑀 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 dom 𝑀 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) ) ) ) ) |
6 |
2 5
|
mpbird |
⊢ ( 𝑀 ∈ ∪ ran measures → 𝑀 ∈ ( measures ‘ dom 𝑀 ) ) |
7 |
|
elfvunirn |
⊢ ( 𝑀 ∈ ( measures ‘ dom 𝑀 ) → 𝑀 ∈ ∪ ran measures ) |
8 |
6 7
|
impbii |
⊢ ( 𝑀 ∈ ∪ ran measures ↔ 𝑀 ∈ ( measures ‘ dom 𝑀 ) ) |