Step |
Hyp |
Ref |
Expression |
1 |
|
elfvdm |
⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑆 ∈ dom measures ) |
2 |
|
vex |
⊢ 𝑠 ∈ V |
3 |
|
ovex |
⊢ ( 0 [,] +∞ ) ∈ V |
4 |
|
mapex |
⊢ ( ( 𝑠 ∈ V ∧ ( 0 [,] +∞ ) ∈ V ) → { 𝑚 ∣ 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) } ∈ V ) |
5 |
2 3 4
|
mp2an |
⊢ { 𝑚 ∣ 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) } ∈ V |
6 |
|
simp1 |
⊢ ( ( 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ) → 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) ) |
7 |
6
|
ss2abi |
⊢ { 𝑚 ∣ ( 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ) } ⊆ { 𝑚 ∣ 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) } |
8 |
5 7
|
ssexi |
⊢ { 𝑚 ∣ ( 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ) } ∈ V |
9 |
|
df-meas |
⊢ measures = ( 𝑠 ∈ ∪ ran sigAlgebra ↦ { 𝑚 ∣ ( 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ) } ) |
10 |
8 9
|
dmmpti |
⊢ dom measures = ∪ ran sigAlgebra |
11 |
1 10
|
eleqtrdi |
⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑆 ∈ ∪ ran sigAlgebra ) |