Step |
Hyp |
Ref |
Expression |
1 |
|
simp2 |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝒫 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝑥 ) ) → 𝐴 ∈ 𝒫 𝑆 ) |
2 |
|
measbase |
⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑆 ∈ ∪ ran sigAlgebra ) |
3 |
|
ismeas |
⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( 𝑀 ∈ ( measures ‘ 𝑆 ) ↔ ( 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑀 ‘ ∅ ) = 0 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( ( 𝑦 ≼ ω ∧ Disj 𝑥 ∈ 𝑦 𝑥 ) → ( 𝑀 ‘ ∪ 𝑦 ) = Σ* 𝑥 ∈ 𝑦 ( 𝑀 ‘ 𝑥 ) ) ) ) ) |
4 |
2 3
|
syl |
⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → ( 𝑀 ∈ ( measures ‘ 𝑆 ) ↔ ( 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑀 ‘ ∅ ) = 0 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( ( 𝑦 ≼ ω ∧ Disj 𝑥 ∈ 𝑦 𝑥 ) → ( 𝑀 ‘ ∪ 𝑦 ) = Σ* 𝑥 ∈ 𝑦 ( 𝑀 ‘ 𝑥 ) ) ) ) ) |
5 |
4
|
ibi |
⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → ( 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑀 ‘ ∅ ) = 0 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( ( 𝑦 ≼ ω ∧ Disj 𝑥 ∈ 𝑦 𝑥 ) → ( 𝑀 ‘ ∪ 𝑦 ) = Σ* 𝑥 ∈ 𝑦 ( 𝑀 ‘ 𝑥 ) ) ) ) |
6 |
5
|
simp3d |
⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → ∀ 𝑦 ∈ 𝒫 𝑆 ( ( 𝑦 ≼ ω ∧ Disj 𝑥 ∈ 𝑦 𝑥 ) → ( 𝑀 ‘ ∪ 𝑦 ) = Σ* 𝑥 ∈ 𝑦 ( 𝑀 ‘ 𝑥 ) ) ) |
7 |
6
|
3ad2ant1 |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝒫 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝑥 ) ) → ∀ 𝑦 ∈ 𝒫 𝑆 ( ( 𝑦 ≼ ω ∧ Disj 𝑥 ∈ 𝑦 𝑥 ) → ( 𝑀 ‘ ∪ 𝑦 ) = Σ* 𝑥 ∈ 𝑦 ( 𝑀 ‘ 𝑥 ) ) ) |
8 |
|
simp3 |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝒫 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝑥 ) ) → ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝑥 ) ) |
9 |
|
breq1 |
⊢ ( 𝑦 = 𝐴 → ( 𝑦 ≼ ω ↔ 𝐴 ≼ ω ) ) |
10 |
|
disjeq1 |
⊢ ( 𝑦 = 𝐴 → ( Disj 𝑥 ∈ 𝑦 𝑥 ↔ Disj 𝑥 ∈ 𝐴 𝑥 ) ) |
11 |
9 10
|
anbi12d |
⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ≼ ω ∧ Disj 𝑥 ∈ 𝑦 𝑥 ) ↔ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝑥 ) ) ) |
12 |
|
unieq |
⊢ ( 𝑦 = 𝐴 → ∪ 𝑦 = ∪ 𝐴 ) |
13 |
12
|
fveq2d |
⊢ ( 𝑦 = 𝐴 → ( 𝑀 ‘ ∪ 𝑦 ) = ( 𝑀 ‘ ∪ 𝐴 ) ) |
14 |
|
esumeq1 |
⊢ ( 𝑦 = 𝐴 → Σ* 𝑥 ∈ 𝑦 ( 𝑀 ‘ 𝑥 ) = Σ* 𝑥 ∈ 𝐴 ( 𝑀 ‘ 𝑥 ) ) |
15 |
13 14
|
eqeq12d |
⊢ ( 𝑦 = 𝐴 → ( ( 𝑀 ‘ ∪ 𝑦 ) = Σ* 𝑥 ∈ 𝑦 ( 𝑀 ‘ 𝑥 ) ↔ ( 𝑀 ‘ ∪ 𝐴 ) = Σ* 𝑥 ∈ 𝐴 ( 𝑀 ‘ 𝑥 ) ) ) |
16 |
11 15
|
imbi12d |
⊢ ( 𝑦 = 𝐴 → ( ( ( 𝑦 ≼ ω ∧ Disj 𝑥 ∈ 𝑦 𝑥 ) → ( 𝑀 ‘ ∪ 𝑦 ) = Σ* 𝑥 ∈ 𝑦 ( 𝑀 ‘ 𝑥 ) ) ↔ ( ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝑥 ) → ( 𝑀 ‘ ∪ 𝐴 ) = Σ* 𝑥 ∈ 𝐴 ( 𝑀 ‘ 𝑥 ) ) ) ) |
17 |
16
|
rspcv |
⊢ ( 𝐴 ∈ 𝒫 𝑆 → ( ∀ 𝑦 ∈ 𝒫 𝑆 ( ( 𝑦 ≼ ω ∧ Disj 𝑥 ∈ 𝑦 𝑥 ) → ( 𝑀 ‘ ∪ 𝑦 ) = Σ* 𝑥 ∈ 𝑦 ( 𝑀 ‘ 𝑥 ) ) → ( ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝑥 ) → ( 𝑀 ‘ ∪ 𝐴 ) = Σ* 𝑥 ∈ 𝐴 ( 𝑀 ‘ 𝑥 ) ) ) ) |
18 |
1 7 8 17
|
syl3c |
⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝒫 𝑆 ∧ ( 𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝑥 ) ) → ( 𝑀 ‘ ∪ 𝐴 ) = Σ* 𝑥 ∈ 𝐴 ( 𝑀 ‘ 𝑥 ) ) |