Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. . . 4
β’ ((π:πβΆ(0[,]+β) β§ (πββ
) = 0 β§
βπ₯ β π«
π((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦))) β π:πβΆ(0[,]+β)) |
2 | 1 | ss2abi 4027 |
. . 3
β’ {π β£ (π:πβΆ(0[,]+β) β§ (πββ
) = 0 β§
βπ₯ β π«
π((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦)))} β {π β£ π:πβΆ(0[,]+β)} |
3 | | ovex 7394 |
. . . 4
β’
(0[,]+β) β V |
4 | | mapex 8777 |
. . . 4
β’ ((π β βͺ ran sigAlgebra β§ (0[,]+β) β V) β
{π β£ π:πβΆ(0[,]+β)} β
V) |
5 | 3, 4 | mpan2 690 |
. . 3
β’ (π β βͺ ran sigAlgebra β {π β£ π:πβΆ(0[,]+β)} β
V) |
6 | | ssexg 5284 |
. . 3
β’ (({π β£ (π:πβΆ(0[,]+β) β§ (πββ
) = 0 β§
βπ₯ β π«
π((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦)))} β {π β£ π:πβΆ(0[,]+β)} β§ {π β£ π:πβΆ(0[,]+β)} β V) β
{π β£ (π:πβΆ(0[,]+β) β§ (πββ
) = 0 β§
βπ₯ β π«
π((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦)))} β V) |
7 | 2, 5, 6 | sylancr 588 |
. 2
β’ (π β βͺ ran sigAlgebra β {π β£ (π:πβΆ(0[,]+β) β§ (πββ
) = 0 β§
βπ₯ β π«
π((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦)))} β V) |
8 | | feq2 6654 |
. . . . 5
β’ (π = π β (π:π βΆ(0[,]+β) β π:πβΆ(0[,]+β))) |
9 | | pweq 4578 |
. . . . . 6
β’ (π = π β π« π = π« π) |
10 | 9 | raleqdv 3312 |
. . . . 5
β’ (π = π β (βπ₯ β π« π ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦)) β βπ₯ β π« π((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦)))) |
11 | 8, 10 | 3anbi13d 1439 |
. . . 4
β’ (π = π β ((π:π βΆ(0[,]+β) β§ (πββ
) = 0 β§
βπ₯ β π«
π ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦))) β (π:πβΆ(0[,]+β) β§ (πββ
) = 0 β§
βπ₯ β π«
π((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦))))) |
12 | 11 | abbidv 2802 |
. . 3
β’ (π = π β {π β£ (π:π βΆ(0[,]+β) β§ (πββ
) = 0 β§
βπ₯ β π«
π ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦)))} = {π β£ (π:πβΆ(0[,]+β) β§ (πββ
) = 0 β§
βπ₯ β π«
π((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦)))}) |
13 | | df-meas 32859 |
. . 3
β’ measures
= (π β βͺ ran sigAlgebra β¦ {π β£ (π:π βΆ(0[,]+β) β§ (πββ
) = 0 β§
βπ₯ β π«
π ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦)))}) |
14 | 12, 13 | fvmptg 6950 |
. 2
β’ ((π β βͺ ran sigAlgebra β§ {π β£ (π:πβΆ(0[,]+β) β§ (πββ
) = 0 β§
βπ₯ β π«
π((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦)))} β V) β (measuresβπ) = {π β£ (π:πβΆ(0[,]+β) β§ (πββ
) = 0 β§
βπ₯ β π«
π((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦)))}) |
15 | 7, 14 | mpdan 686 |
1
β’ (π β βͺ ran sigAlgebra β (measuresβπ) = {π β£ (π:πβΆ(0[,]+β) β§ (πββ
) = 0 β§
βπ₯ β π«
π((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦)))}) |