Step | Hyp | Ref
| Expression |
1 | | omsmon.a |
. . . . . . . . . . 11
β’ (π β π΄ β π΅) |
2 | 1 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π§ β π« dom π
) β π΄ β π΅) |
3 | | sstr2 3990 |
. . . . . . . . . 10
β’ (π΄ β π΅ β (π΅ β βͺ π§ β π΄ β βͺ π§)) |
4 | 2, 3 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π§ β π« dom π
) β (π΅ β βͺ π§ β π΄ β βͺ π§)) |
5 | 4 | anim1d 612 |
. . . . . . . 8
β’ ((π β§ π§ β π« dom π
) β ((π΅ β βͺ π§ β§ π§ βΌ Ο) β (π΄ β βͺ π§ β§ π§ βΌ Ο))) |
6 | 5 | ss2rabdv 4074 |
. . . . . . 7
β’ (π β {π§ β π« dom π
β£ (π΅ β βͺ π§ β§ π§ βΌ Ο)} β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)}) |
7 | | resmpt 6038 |
. . . . . . 7
β’ ({π§ β π« dom π
β£ (π΅ β βͺ π§ β§ π§ βΌ Ο)} β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β ((π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)) βΎ {π§ β π« dom π
β£ (π΅ β βͺ π§ β§ π§ βΌ Ο)}) = (π₯ β {π§ β π« dom π
β£ (π΅ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦))) |
8 | 6, 7 | syl 17 |
. . . . . 6
β’ (π β ((π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)) βΎ {π§ β π« dom π
β£ (π΅ β βͺ π§ β§ π§ βΌ Ο)}) = (π₯ β {π§ β π« dom π
β£ (π΅ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦))) |
9 | | resss 6007 |
. . . . . 6
β’ ((π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)) βΎ {π§ β π« dom π
β£ (π΅ β βͺ π§ β§ π§ βΌ Ο)}) β (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)) |
10 | 8, 9 | eqsstrrdi 4038 |
. . . . 5
β’ (π β (π₯ β {π§ β π« dom π
β£ (π΅ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)) β (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦))) |
11 | | rnss 5939 |
. . . . 5
β’ ((π₯ β {π§ β π« dom π
β£ (π΅ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)) β (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)) β ran (π₯ β {π§ β π« dom π
β£ (π΅ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)) β ran (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦))) |
12 | 10, 11 | syl 17 |
. . . 4
β’ (π β ran (π₯ β {π§ β π« dom π
β£ (π΅ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)) β ran (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦))) |
13 | | oms.r |
. . . . . . . . . 10
β’ (π β π
:πβΆ(0[,]+β)) |
14 | 13 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)}) β§ π¦ β π₯) β π
:πβΆ(0[,]+β)) |
15 | | ssrab2 4078 |
. . . . . . . . . . . . 13
β’ {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β π« dom
π
|
16 | | simplr 768 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)}) β§ π¦ β π₯) β π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)}) |
17 | 15, 16 | sselid 3981 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)}) β§ π¦ β π₯) β π₯ β π« dom π
) |
18 | | elpwi 4610 |
. . . . . . . . . . . 12
β’ (π₯ β π« dom π
β π₯ β dom π
) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)}) β§ π¦ β π₯) β π₯ β dom π
) |
20 | 13 | fdmd 6729 |
. . . . . . . . . . . 12
β’ (π β dom π
= π) |
21 | 20 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)}) β§ π¦ β π₯) β dom π
= π) |
22 | 19, 21 | sseqtrd 4023 |
. . . . . . . . . 10
β’ (((π β§ π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)}) β§ π¦ β π₯) β π₯ β π) |
23 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)}) β§ π¦ β π₯) β π¦ β π₯) |
24 | 22, 23 | sseldd 3984 |
. . . . . . . . 9
β’ (((π β§ π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)}) β§ π¦ β π₯) β π¦ β π) |
25 | 14, 24 | ffvelcdmd 7088 |
. . . . . . . 8
β’ (((π β§ π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)}) β§ π¦ β π₯) β (π
βπ¦) β (0[,]+β)) |
26 | 25 | ralrimiva 3147 |
. . . . . . 7
β’ ((π β§ π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)}) β βπ¦ β π₯ (π
βπ¦) β (0[,]+β)) |
27 | | vex 3479 |
. . . . . . . 8
β’ π₯ β V |
28 | | nfcv 2904 |
. . . . . . . . 9
β’
β²π¦π₯ |
29 | 28 | esumcl 33028 |
. . . . . . . 8
β’ ((π₯ β V β§ βπ¦ β π₯ (π
βπ¦) β (0[,]+β)) β
Ξ£*π¦ β
π₯(π
βπ¦) β (0[,]+β)) |
30 | 27, 29 | mpan 689 |
. . . . . . 7
β’
(βπ¦ β
π₯ (π
βπ¦) β (0[,]+β) β
Ξ£*π¦ β
π₯(π
βπ¦) β (0[,]+β)) |
31 | 26, 30 | syl 17 |
. . . . . 6
β’ ((π β§ π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)}) β
Ξ£*π¦ β
π₯(π
βπ¦) β (0[,]+β)) |
32 | 31 | ralrimiva 3147 |
. . . . 5
β’ (π β βπ₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)}Ξ£*π¦ β π₯(π
βπ¦) β (0[,]+β)) |
33 | | eqid 2733 |
. . . . . 6
β’ (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)) = (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)) |
34 | 33 | rnmptss 7122 |
. . . . 5
β’
(βπ₯ β
{π§ β π« dom
π
β£ (π΄ β βͺ π§
β§ π§ βΌ
Ο)}Ξ£*π¦ β π₯(π
βπ¦) β (0[,]+β) β ran (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)) β (0[,]+β)) |
35 | 32, 34 | syl 17 |
. . . 4
β’ (π β ran (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)) β (0[,]+β)) |
36 | 12, 35 | xrge0infssd 31974 |
. . 3
β’ (π β inf(ran (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)), (0[,]+β), < ) β€ inf(ran
(π₯ β {π§ β π« dom π
β£ (π΅ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)), (0[,]+β), < )) |
37 | | oms.o |
. . . 4
β’ (π β π β π) |
38 | | omsmon.b |
. . . . 5
β’ (π β π΅ β βͺ π) |
39 | 1, 38 | sstrd 3993 |
. . . 4
β’ (π β π΄ β βͺ π) |
40 | | omsfval 33293 |
. . . 4
β’ ((π β π β§ π
:πβΆ(0[,]+β) β§ π΄ β βͺ π)
β ((toOMeasβπ
)βπ΄) = inf(ran (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)), (0[,]+β), < )) |
41 | 37, 13, 39, 40 | syl3anc 1372 |
. . 3
β’ (π β ((toOMeasβπ
)βπ΄) = inf(ran (π₯ β {π§ β π« dom π
β£ (π΄ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)), (0[,]+β), < )) |
42 | | omsfval 33293 |
. . . 4
β’ ((π β π β§ π
:πβΆ(0[,]+β) β§ π΅ β βͺ π)
β ((toOMeasβπ
)βπ΅) = inf(ran (π₯ β {π§ β π« dom π
β£ (π΅ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)), (0[,]+β), < )) |
43 | 37, 13, 38, 42 | syl3anc 1372 |
. . 3
β’ (π β ((toOMeasβπ
)βπ΅) = inf(ran (π₯ β {π§ β π« dom π
β£ (π΅ β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)), (0[,]+β), < )) |
44 | 36, 41, 43 | 3brtr4d 5181 |
. 2
β’ (π β ((toOMeasβπ
)βπ΄) β€ ((toOMeasβπ
)βπ΅)) |
45 | | oms.m |
. . 3
β’ π = (toOMeasβπ
) |
46 | 45 | fveq1i 6893 |
. 2
β’ (πβπ΄) = ((toOMeasβπ
)βπ΄) |
47 | 45 | fveq1i 6893 |
. 2
β’ (πβπ΅) = ((toOMeasβπ
)βπ΅) |
48 | 44, 46, 47 | 3brtr4g 5183 |
1
β’ (π β (πβπ΄) β€ (πβπ΅)) |