Step | Hyp | Ref
| Expression |
1 | | iccssxr 13353 |
. . . . 5
β’
(0[,]+β) β β* |
2 | | xrltso 13066 |
. . . . 5
β’ < Or
β* |
3 | | soss 5566 |
. . . . 5
β’
((0[,]+β) β β* β ( < Or
β* β < Or (0[,]+β))) |
4 | 1, 2, 3 | mp2 9 |
. . . 4
β’ < Or
(0[,]+β) |
5 | 4 | a1i 11 |
. . 3
β’ (((π β π β§ π
:πβΆ(0[,]+β)) β§ π β π« βͺ dom π
) β < Or
(0[,]+β)) |
6 | | omscl 32952 |
. . . . 5
β’ ((π β π β§ π
:πβΆ(0[,]+β) β§ π β π« βͺ dom π
) β ran (π₯ β {π§ β π« dom π
β£ (π β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)) β (0[,]+β)) |
7 | 6 | 3expa 1119 |
. . . 4
β’ (((π β π β§ π
:πβΆ(0[,]+β)) β§ π β π« βͺ dom π
) β ran (π₯ β {π§ β π« dom π
β£ (π β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)) β (0[,]+β)) |
8 | | xrge0infss 31712 |
. . . 4
β’ (ran
(π₯ β {π§ β π« dom π
β£ (π β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)) β (0[,]+β) β βπ‘ β
(0[,]+β)(βπ€
β ran (π₯ β {π§ β π« dom π
β£ (π β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)) Β¬ π€ < π‘ β§ βπ€ β (0[,]+β)(π‘ < π€ β βπ β ran (π₯ β {π§ β π« dom π
β£ (π β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦))π < π€))) |
9 | 7, 8 | syl 17 |
. . 3
β’ (((π β π β§ π
:πβΆ(0[,]+β)) β§ π β π« βͺ dom π
) β βπ‘ β (0[,]+β)(βπ€ β ran (π₯ β {π§ β π« dom π
β£ (π β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)) Β¬ π€ < π‘ β§ βπ€ β (0[,]+β)(π‘ < π€ β βπ β ran (π₯ β {π§ β π« dom π
β£ (π β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦))π < π€))) |
10 | 5, 9 | infcl 9429 |
. 2
β’ (((π β π β§ π
:πβΆ(0[,]+β)) β§ π β π« βͺ dom π
) β inf(ran (π₯ β {π§ β π« dom π
β£ (π β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)), (0[,]+β), < ) β
(0[,]+β)) |
11 | | fex 7177 |
. . . 4
β’ ((π
:πβΆ(0[,]+β) β§ π β π) β π
β V) |
12 | 11 | ancoms 460 |
. . 3
β’ ((π β π β§ π
:πβΆ(0[,]+β)) β π
β V) |
13 | | omsval 32950 |
. . 3
β’ (π
β V β
(toOMeasβπ
) = (π β π« βͺ dom π
β¦ inf(ran (π₯ β {π§ β π« dom π
β£ (π β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)), (0[,]+β), < ))) |
14 | 12, 13 | syl 17 |
. 2
β’ ((π β π β§ π
:πβΆ(0[,]+β)) β
(toOMeasβπ
) = (π β π« βͺ dom π
β¦ inf(ran (π₯ β {π§ β π« dom π
β£ (π β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)), (0[,]+β), < ))) |
15 | | simpll 766 |
. . . 4
β’ (((π β π β§ π
:πβΆ(0[,]+β)) β§ π β π« βͺ dom π
) β π β π) |
16 | | simplr 768 |
. . . 4
β’ (((π β π β§ π
:πβΆ(0[,]+β)) β§ π β π« βͺ dom π
) β π
:πβΆ(0[,]+β)) |
17 | | simpr 486 |
. . . . . 6
β’ (((π β π β§ π
:πβΆ(0[,]+β)) β§ π β π« βͺ dom π
) β π β π« βͺ dom π
) |
18 | | fdm 6678 |
. . . . . . . . 9
β’ (π
:πβΆ(0[,]+β) β dom π
= π) |
19 | 18 | unieqd 4880 |
. . . . . . . 8
β’ (π
:πβΆ(0[,]+β) β βͺ dom π
= βͺ π) |
20 | 19 | pweqd 4578 |
. . . . . . 7
β’ (π
:πβΆ(0[,]+β) β π«
βͺ dom π
= π« βͺ
π) |
21 | 20 | ad2antlr 726 |
. . . . . 6
β’ (((π β π β§ π
:πβΆ(0[,]+β)) β§ π β π« βͺ dom π
) β π« βͺ dom π
= π« βͺ
π) |
22 | 17, 21 | eleqtrd 2836 |
. . . . 5
β’ (((π β π β§ π
:πβΆ(0[,]+β)) β§ π β π« βͺ dom π
) β π β π« βͺ π) |
23 | | elpwi 4568 |
. . . . 5
β’ (π β π« βͺ π
β π β βͺ π) |
24 | 22, 23 | syl 17 |
. . . 4
β’ (((π β π β§ π
:πβΆ(0[,]+β)) β§ π β π« βͺ dom π
) β π β βͺ π) |
25 | | omsfval 32951 |
. . . 4
β’ ((π β π β§ π
:πβΆ(0[,]+β) β§ π β βͺ π)
β ((toOMeasβπ
)βπ) = inf(ran (π₯ β {π§ β π« dom π
β£ (π β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)), (0[,]+β), < )) |
26 | 15, 16, 24, 25 | syl3anc 1372 |
. . 3
β’ (((π β π β§ π
:πβΆ(0[,]+β)) β§ π β π« βͺ dom π
) β ((toOMeasβπ
)βπ) = inf(ran (π₯ β {π§ β π« dom π
β£ (π β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)), (0[,]+β), < )) |
27 | 26, 10 | eqeltrd 2834 |
. 2
β’ (((π β π β§ π
:πβΆ(0[,]+β)) β§ π β π« βͺ dom π
) β ((toOMeasβπ
)βπ) β (0[,]+β)) |
28 | 10, 14, 27 | fmpt2d 7072 |
1
β’ ((π β π β§ π
:πβΆ(0[,]+β)) β
(toOMeasβπ
):π«
βͺ dom π
βΆ(0[,]+β)) |