Step |
Hyp |
Ref |
Expression |
1 |
|
i1ff |
|- ( F e. dom S.1 -> F : RR --> RR ) |
2 |
|
xrge0f |
|- ( ( F : RR --> RR /\ 0p oR <_ F ) -> F : RR --> ( 0 [,] +oo ) ) |
3 |
1 2
|
sylan |
|- ( ( F e. dom S.1 /\ 0p oR <_ F ) -> F : RR --> ( 0 [,] +oo ) ) |
4 |
|
itg2cl |
|- ( F : RR --> ( 0 [,] +oo ) -> ( S.2 ` F ) e. RR* ) |
5 |
3 4
|
syl |
|- ( ( F e. dom S.1 /\ 0p oR <_ F ) -> ( S.2 ` F ) e. RR* ) |
6 |
|
itg1cl |
|- ( F e. dom S.1 -> ( S.1 ` F ) e. RR ) |
7 |
6
|
adantr |
|- ( ( F e. dom S.1 /\ 0p oR <_ F ) -> ( S.1 ` F ) e. RR ) |
8 |
7
|
rexrd |
|- ( ( F e. dom S.1 /\ 0p oR <_ F ) -> ( S.1 ` F ) e. RR* ) |
9 |
|
itg1le |
|- ( ( g e. dom S.1 /\ F e. dom S.1 /\ g oR <_ F ) -> ( S.1 ` g ) <_ ( S.1 ` F ) ) |
10 |
9
|
3expia |
|- ( ( g e. dom S.1 /\ F e. dom S.1 ) -> ( g oR <_ F -> ( S.1 ` g ) <_ ( S.1 ` F ) ) ) |
11 |
10
|
ancoms |
|- ( ( F e. dom S.1 /\ g e. dom S.1 ) -> ( g oR <_ F -> ( S.1 ` g ) <_ ( S.1 ` F ) ) ) |
12 |
11
|
ralrimiva |
|- ( F e. dom S.1 -> A. g e. dom S.1 ( g oR <_ F -> ( S.1 ` g ) <_ ( S.1 ` F ) ) ) |
13 |
12
|
adantr |
|- ( ( F e. dom S.1 /\ 0p oR <_ F ) -> A. g e. dom S.1 ( g oR <_ F -> ( S.1 ` g ) <_ ( S.1 ` F ) ) ) |
14 |
|
itg2leub |
|- ( ( F : RR --> ( 0 [,] +oo ) /\ ( S.1 ` F ) e. RR* ) -> ( ( S.2 ` F ) <_ ( S.1 ` F ) <-> A. g e. dom S.1 ( g oR <_ F -> ( S.1 ` g ) <_ ( S.1 ` F ) ) ) ) |
15 |
3 8 14
|
syl2anc |
|- ( ( F e. dom S.1 /\ 0p oR <_ F ) -> ( ( S.2 ` F ) <_ ( S.1 ` F ) <-> A. g e. dom S.1 ( g oR <_ F -> ( S.1 ` g ) <_ ( S.1 ` F ) ) ) ) |
16 |
13 15
|
mpbird |
|- ( ( F e. dom S.1 /\ 0p oR <_ F ) -> ( S.2 ` F ) <_ ( S.1 ` F ) ) |
17 |
|
simpl |
|- ( ( F e. dom S.1 /\ 0p oR <_ F ) -> F e. dom S.1 ) |
18 |
|
reex |
|- RR e. _V |
19 |
18
|
a1i |
|- ( F e. dom S.1 -> RR e. _V ) |
20 |
|
leid |
|- ( x e. RR -> x <_ x ) |
21 |
20
|
adantl |
|- ( ( F e. dom S.1 /\ x e. RR ) -> x <_ x ) |
22 |
19 1 21
|
caofref |
|- ( F e. dom S.1 -> F oR <_ F ) |
23 |
22
|
adantr |
|- ( ( F e. dom S.1 /\ 0p oR <_ F ) -> F oR <_ F ) |
24 |
|
itg2ub |
|- ( ( F : RR --> ( 0 [,] +oo ) /\ F e. dom S.1 /\ F oR <_ F ) -> ( S.1 ` F ) <_ ( S.2 ` F ) ) |
25 |
3 17 23 24
|
syl3anc |
|- ( ( F e. dom S.1 /\ 0p oR <_ F ) -> ( S.1 ` F ) <_ ( S.2 ` F ) ) |
26 |
5 8 16 25
|
xrletrid |
|- ( ( F e. dom S.1 /\ 0p oR <_ F ) -> ( S.2 ` F ) = ( S.1 ` F ) ) |