Metamath Proof Explorer

Theorem itg2monolem2

Description: Lemma for itg2mono . (Contributed by Mario Carneiro, 16-Aug-2014)

Ref Expression
Hypotheses itg2mono.1 
|- G = ( x e. RR |-> sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) )
itg2mono.2 
|- ( ( ph /\ n e. NN ) -> ( F ` n ) e. MblFn )
itg2mono.3 
|- ( ( ph /\ n e. NN ) -> ( F ` n ) : RR --> ( 0 [,) +oo ) )
itg2mono.4 
|- ( ( ph /\ n e. NN ) -> ( F ` n ) oR <_ ( F ` ( n + 1 ) ) )
itg2mono.5 
|- ( ( ph /\ x e. RR ) -> E. y e. RR A. n e. NN ( ( F ` n ) ` x ) <_ y )
itg2mono.6 
|- S = sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < )
itg2monolem2.7 
|- ( ph -> P e. dom S.1 )
itg2monolem2.8 
|- ( ph -> P oR <_ G )
itg2monolem2.9 
|- ( ph -> -. ( S.1 ` P ) <_ S )
Assertion itg2monolem2 
|- ( ph -> S e. RR )

Proof

Step Hyp Ref Expression
1 itg2mono.1 
 |-  G = ( x e. RR |-> sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) )
2 itg2mono.2 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) e. MblFn )
3 itg2mono.3 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) : RR --> ( 0 [,) +oo ) )
4 itg2mono.4 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) oR <_ ( F ` ( n + 1 ) ) )
5 itg2mono.5 
 |-  ( ( ph /\ x e. RR ) -> E. y e. RR A. n e. NN ( ( F ` n ) ` x ) <_ y )
6 itg2mono.6 
 |-  S = sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < )
7 itg2monolem2.7 
 |-  ( ph -> P e. dom S.1 )
8 itg2monolem2.8 
 |-  ( ph -> P oR <_ G )
9 itg2monolem2.9 
 |-  ( ph -> -. ( S.1 ` P ) <_ S )
10 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
11 fss 
 |-  ( ( ( F ` n ) : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ ( 0 [,] +oo ) ) -> ( F ` n ) : RR --> ( 0 [,] +oo ) )
12 3 10 11 sylancl 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) : RR --> ( 0 [,] +oo ) )
13 itg2cl 
 |-  ( ( F ` n ) : RR --> ( 0 [,] +oo ) -> ( S.2 ` ( F ` n ) ) e. RR* )
14 12 13 syl 
 |-  ( ( ph /\ n e. NN ) -> ( S.2 ` ( F ` n ) ) e. RR* )
15 14 fmpttd 
 |-  ( ph -> ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) : NN --> RR* )
16 15 frnd 
 |-  ( ph -> ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) C_ RR* )
17 supxrcl 
 |-  ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) C_ RR* -> sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < ) e. RR* )
18 16 17 syl 
 |-  ( ph -> sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < ) e. RR* )
19 6 18 eqeltrid 
 |-  ( ph -> S e. RR* )
20 itg1cl 
 |-  ( P e. dom S.1 -> ( S.1 ` P ) e. RR )
21 7 20 syl 
 |-  ( ph -> ( S.1 ` P ) e. RR )
22 mnfxr 
 |-  -oo e. RR*
23 22 a1i 
 |-  ( ph -> -oo e. RR* )
24 fveq2 
 |-  ( n = 1 -> ( F ` n ) = ( F ` 1 ) )
25 24 feq1d 
 |-  ( n = 1 -> ( ( F ` n ) : RR --> ( 0 [,] +oo ) <-> ( F ` 1 ) : RR --> ( 0 [,] +oo ) ) )
26 12 ralrimiva 
 |-  ( ph -> A. n e. NN ( F ` n ) : RR --> ( 0 [,] +oo ) )
27 1nn 
 |-  1 e. NN
28 27 a1i 
 |-  ( ph -> 1 e. NN )
29 25 26 28 rspcdva 
 |-  ( ph -> ( F ` 1 ) : RR --> ( 0 [,] +oo ) )
30 itg2cl 
 |-  ( ( F ` 1 ) : RR --> ( 0 [,] +oo ) -> ( S.2 ` ( F ` 1 ) ) e. RR* )
31 29 30 syl 
 |-  ( ph -> ( S.2 ` ( F ` 1 ) ) e. RR* )
32 itg2ge0 
 |-  ( ( F ` 1 ) : RR --> ( 0 [,] +oo ) -> 0 <_ ( S.2 ` ( F ` 1 ) ) )
33 29 32 syl 
 |-  ( ph -> 0 <_ ( S.2 ` ( F ` 1 ) ) )
34 mnflt0 
 |-  -oo < 0
35 0xr 
 |-  0 e. RR*
36 xrltletr 
 |-  ( ( -oo e. RR* /\ 0 e. RR* /\ ( S.2 ` ( F ` 1 ) ) e. RR* ) -> ( ( -oo < 0 /\ 0 <_ ( S.2 ` ( F ` 1 ) ) ) -> -oo < ( S.2 ` ( F ` 1 ) ) ) )
37 22 35 31 36 mp3an12i 
 |-  ( ph -> ( ( -oo < 0 /\ 0 <_ ( S.2 ` ( F ` 1 ) ) ) -> -oo < ( S.2 ` ( F ` 1 ) ) ) )
38 34 37 mpani 
 |-  ( ph -> ( 0 <_ ( S.2 ` ( F ` 1 ) ) -> -oo < ( S.2 ` ( F ` 1 ) ) ) )
39 33 38 mpd 
 |-  ( ph -> -oo < ( S.2 ` ( F ` 1 ) ) )
40 2fveq3 
 |-  ( n = 1 -> ( S.2 ` ( F ` n ) ) = ( S.2 ` ( F ` 1 ) ) )
41 eqid 
 |-  ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) = ( n e. NN |-> ( S.2 ` ( F ` n ) ) )
42 fvex 
 |-  ( S.2 ` ( F ` 1 ) ) e. _V
43 40 41 42 fvmpt 
 |-  ( 1 e. NN -> ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` 1 ) = ( S.2 ` ( F ` 1 ) ) )
44 27 43 ax-mp 
 |-  ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` 1 ) = ( S.2 ` ( F ` 1 ) )
45 15 ffnd 
 |-  ( ph -> ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) Fn NN )
46 fnfvelrn 
 |-  ( ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) Fn NN /\ 1 e. NN ) -> ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` 1 ) e. ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) )
47 45 27 46 sylancl 
 |-  ( ph -> ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` 1 ) e. ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) )
48 44 47 eqeltrrid 
 |-  ( ph -> ( S.2 ` ( F ` 1 ) ) e. ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) )
49 supxrub 
 |-  ( ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) C_ RR* /\ ( S.2 ` ( F ` 1 ) ) e. ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ) -> ( S.2 ` ( F ` 1 ) ) <_ sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < ) )
50 16 48 49 syl2anc 
 |-  ( ph -> ( S.2 ` ( F ` 1 ) ) <_ sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < ) )
51 50 6 breqtrrdi 
 |-  ( ph -> ( S.2 ` ( F ` 1 ) ) <_ S )
52 23 31 19 39 51 xrltletrd 
 |-  ( ph -> -oo < S )
53 21 rexrd 
 |-  ( ph -> ( S.1 ` P ) e. RR* )
54 xrltnle 
 |-  ( ( S e. RR* /\ ( S.1 ` P ) e. RR* ) -> ( S < ( S.1 ` P ) <-> -. ( S.1 ` P ) <_ S ) )
55 19 53 54 syl2anc 
 |-  ( ph -> ( S < ( S.1 ` P ) <-> -. ( S.1 ` P ) <_ S ) )
56 9 55 mpbird 
 |-  ( ph -> S < ( S.1 ` P ) )
57 19 53 56 xrltled 
 |-  ( ph -> S <_ ( S.1 ` P ) )
58 xrre 
 |-  ( ( ( S e. RR* /\ ( S.1 ` P ) e. RR ) /\ ( -oo < S /\ S <_ ( S.1 ` P ) ) ) -> S e. RR )
59 19 21 52 57 58 syl22anc 
 |-  ( ph -> S e. RR )