Metamath Proof Explorer

Theorem liminflelimsuplem

Description: The superior limit is greater than or equal to the inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses liminflelimsuplem.1 
|- ( ph -> F e. V )
liminflelimsuplem.2 
|- ( ph -> A. k e. RR E. j e. ( k [,) +oo ) ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) )
Assertion liminflelimsuplem 
|- ( ph -> ( liminf ` F ) <_ ( limsup ` F ) )

Proof

Step Hyp Ref Expression
1 liminflelimsuplem.1 
 |-  ( ph -> F e. V )
2 liminflelimsuplem.2 
 |-  ( ph -> A. k e. RR E. j e. ( k [,) +oo ) ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) )
3 simpr 
 |-  ( ( i e. RR /\ l e. RR ) -> l e. RR )
4 simpl 
 |-  ( ( i e. RR /\ l e. RR ) -> i e. RR )
5 3 4 ifcld 
 |-  ( ( i e. RR /\ l e. RR ) -> if ( i <_ l , l , i ) e. RR )
6 5 adantll 
 |-  ( ( ( ph /\ i e. RR ) /\ l e. RR ) -> if ( i <_ l , l , i ) e. RR )
7 2 ad2antrr 
 |-  ( ( ( ph /\ i e. RR ) /\ l e. RR ) -> A. k e. RR E. j e. ( k [,) +oo ) ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) )
8 oveq1 
 |-  ( k = if ( i <_ l , l , i ) -> ( k [,) +oo ) = ( if ( i <_ l , l , i ) [,) +oo ) )
9 8 rexeqdv 
 |-  ( k = if ( i <_ l , l , i ) -> ( E. j e. ( k [,) +oo ) ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) <-> E. j e. ( if ( i <_ l , l , i ) [,) +oo ) ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) ) )
10 9 rspcva 
 |-  ( ( if ( i <_ l , l , i ) e. RR /\ A. k e. RR E. j e. ( k [,) +oo ) ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) ) -> E. j e. ( if ( i <_ l , l , i ) [,) +oo ) ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) )
11 6 7 10 syl2anc 
 |-  ( ( ( ph /\ i e. RR ) /\ l e. RR ) -> E. j e. ( if ( i <_ l , l , i ) [,) +oo ) ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) )
12 inss2 
 |-  ( ( F " ( i [,) +oo ) ) i^i RR* ) C_ RR*
13 infxrcl 
 |-  ( ( ( F " ( i [,) +oo ) ) i^i RR* ) C_ RR* -> inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR* )
14 12 13 ax-mp 
 |-  inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR*
15 14 a1i 
 |-  ( ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) /\ ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) ) -> inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR* )
16 inss2 
 |-  ( ( F " ( j [,) +oo ) ) i^i RR* ) C_ RR*
17 infxrcl 
 |-  ( ( ( F " ( j [,) +oo ) ) i^i RR* ) C_ RR* -> inf ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR* )
18 16 17 ax-mp 
 |-  inf ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR*
19 18 a1i 
 |-  ( ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) /\ ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) ) -> inf ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR* )
20 inss2 
 |-  ( ( F " ( l [,) +oo ) ) i^i RR* ) C_ RR*
21 supxrcl 
 |-  ( ( ( F " ( l [,) +oo ) ) i^i RR* ) C_ RR* -> sup ( ( ( F " ( l [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR* )
22 20 21 ax-mp 
 |-  sup ( ( ( F " ( l [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR*
23 22 a1i 
 |-  ( ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) /\ ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) ) -> sup ( ( ( F " ( l [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR* )
24 rexr 
 |-  ( i e. RR -> i e. RR* )
25 24 ad2antrr 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> i e. RR* )
26 pnfxr 
 |-  +oo e. RR*
27 26 a1i 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> +oo e. RR* )
28 5 rexrd 
 |-  ( ( i e. RR /\ l e. RR ) -> if ( i <_ l , l , i ) e. RR* )
29 28 adantr 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> if ( i <_ l , l , i ) e. RR* )
30 icossxr 
 |-  ( if ( i <_ l , l , i ) [,) +oo ) C_ RR*
31 id 
 |-  ( j e. ( if ( i <_ l , l , i ) [,) +oo ) -> j e. ( if ( i <_ l , l , i ) [,) +oo ) )
32 30 31 sseldi 
 |-  ( j e. ( if ( i <_ l , l , i ) [,) +oo ) -> j e. RR* )
33 32 adantl 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> j e. RR* )
34 max1 
 |-  ( ( i e. RR /\ l e. RR ) -> i <_ if ( i <_ l , l , i ) )
35 34 adantr 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> i <_ if ( i <_ l , l , i ) )
36 simpr 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> j e. ( if ( i <_ l , l , i ) [,) +oo ) )
37 29 27 36 icogelbd 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> if ( i <_ l , l , i ) <_ j )
38 25 29 33 35 37 xrletrd 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> i <_ j )
39 25 27 38 icossico2 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> ( j [,) +oo ) C_ ( i [,) +oo ) )
40 39 imass2d 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> ( F " ( j [,) +oo ) ) C_ ( F " ( i [,) +oo ) ) )
41 40 ssrind 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> ( ( F " ( j [,) +oo ) ) i^i RR* ) C_ ( ( F " ( i [,) +oo ) ) i^i RR* ) )
42 12 a1i 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> ( ( F " ( i [,) +oo ) ) i^i RR* ) C_ RR* )
43 infxrss 
 |-  ( ( ( ( F " ( j [,) +oo ) ) i^i RR* ) C_ ( ( F " ( i [,) +oo ) ) i^i RR* ) /\ ( ( F " ( i [,) +oo ) ) i^i RR* ) C_ RR* ) -> inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) <_ inf ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) )
44 41 42 43 syl2anc 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) <_ inf ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) )
45 44 adantr 
 |-  ( ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) /\ ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) ) -> inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) <_ inf ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) )
46 supxrcl 
 |-  ( ( ( F " ( j [,) +oo ) ) i^i RR* ) C_ RR* -> sup ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR* )
47 16 46 ax-mp 
 |-  sup ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR*
48 47 a1i 
 |-  ( ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) /\ ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) ) -> sup ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR* )
49 16 a1i 
 |-  ( ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) /\ ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) ) -> ( ( F " ( j [,) +oo ) ) i^i RR* ) C_ RR* )
50 simpr 
 |-  ( ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) /\ ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) ) -> ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) )
51 49 50 infxrlesupxr 
 |-  ( ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) /\ ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) ) -> inf ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) <_ sup ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) )
52 rexr 
 |-  ( l e. RR -> l e. RR* )
53 52 ad2antlr 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> l e. RR* )
54 max2 
 |-  ( ( i e. RR /\ l e. RR ) -> l <_ if ( i <_ l , l , i ) )
55 54 adantr 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> l <_ if ( i <_ l , l , i ) )
56 53 29 33 55 37 xrletrd 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> l <_ j )
57 53 27 56 icossico2 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> ( j [,) +oo ) C_ ( l [,) +oo ) )
58 57 imass2d 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> ( F " ( j [,) +oo ) ) C_ ( F " ( l [,) +oo ) ) )
59 58 ssrind 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> ( ( F " ( j [,) +oo ) ) i^i RR* ) C_ ( ( F " ( l [,) +oo ) ) i^i RR* ) )
60 20 a1i 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> ( ( F " ( l [,) +oo ) ) i^i RR* ) C_ RR* )
61 supxrss 
 |-  ( ( ( ( F " ( j [,) +oo ) ) i^i RR* ) C_ ( ( F " ( l [,) +oo ) ) i^i RR* ) /\ ( ( F " ( l [,) +oo ) ) i^i RR* ) C_ RR* ) -> sup ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) <_ sup ( ( ( F " ( l [,) +oo ) ) i^i RR* ) , RR* , < ) )
62 59 60 61 syl2anc 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> sup ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) <_ sup ( ( ( F " ( l [,) +oo ) ) i^i RR* ) , RR* , < ) )
63 62 adantr 
 |-  ( ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) /\ ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) ) -> sup ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) <_ sup ( ( ( F " ( l [,) +oo ) ) i^i RR* ) , RR* , < ) )
64 19 48 23 51 63 xrletrd 
 |-  ( ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) /\ ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) ) -> inf ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) <_ sup ( ( ( F " ( l [,) +oo ) ) i^i RR* ) , RR* , < ) )
65 15 19 23 45 64 xrletrd 
 |-  ( ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) /\ ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) ) -> inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) <_ sup ( ( ( F " ( l [,) +oo ) ) i^i RR* ) , RR* , < ) )
66 65 ad5ant2345 
 |-  ( ( ( ( ( ph /\ i e. RR ) /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) /\ ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) ) -> inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) <_ sup ( ( ( F " ( l [,) +oo ) ) i^i RR* ) , RR* , < ) )
67 66 rexlimdva2 
 |-  ( ( ( ph /\ i e. RR ) /\ l e. RR ) -> ( E. j e. ( if ( i <_ l , l , i ) [,) +oo ) ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) -> inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) <_ sup ( ( ( F " ( l [,) +oo ) ) i^i RR* ) , RR* , < ) ) )
68 11 67 mpd 
 |-  ( ( ( ph /\ i e. RR ) /\ l e. RR ) -> inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) <_ sup ( ( ( F " ( l [,) +oo ) ) i^i RR* ) , RR* , < ) )
69 68 ralrimiva 
 |-  ( ( ph /\ i e. RR ) -> A. l e. RR inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) <_ sup ( ( ( F " ( l [,) +oo ) ) i^i RR* ) , RR* , < ) )
70 nfv 
 |-  F/ l ph
71 xrltso 
 |-  < Or RR*
72 71 supex 
 |-  sup ( ( ( F " ( l [,) +oo ) ) i^i RR* ) , RR* , < ) e. _V
73 72 a1i 
 |-  ( ( ph /\ l e. RR ) -> sup ( ( ( F " ( l [,) +oo ) ) i^i RR* ) , RR* , < ) e. _V )
74 breq2 
 |-  ( y = sup ( ( ( F " ( l [,) +oo ) ) i^i RR* ) , RR* , < ) -> ( inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) <_ y <-> inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) <_ sup ( ( ( F " ( l [,) +oo ) ) i^i RR* ) , RR* , < ) ) )
75 70 73 74 ralrnmpt3 
 |-  ( ph -> ( A. y e. ran ( l e. RR |-> sup ( ( ( F " ( l [,) +oo ) ) i^i RR* ) , RR* , < ) ) inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) <_ y <-> A. l e. RR inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) <_ sup ( ( ( F " ( l [,) +oo ) ) i^i RR* ) , RR* , < ) ) )
76 75 adantr 
 |-  ( ( ph /\ i e. RR ) -> ( A. y e. ran ( l e. RR |-> sup ( ( ( F " ( l [,) +oo ) ) i^i RR* ) , RR* , < ) ) inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) <_ y <-> A. l e. RR inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) <_ sup ( ( ( F " ( l [,) +oo ) ) i^i RR* ) , RR* , < ) ) )
77 69 76 mpbird 
 |-  ( ( ph /\ i e. RR ) -> A. y e. ran ( l e. RR |-> sup ( ( ( F " ( l [,) +oo ) ) i^i RR* ) , RR* , < ) ) inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) <_ y )
78 oveq1 
 |-  ( l = i -> ( l [,) +oo ) = ( i [,) +oo ) )
79 78 imaeq2d 
 |-  ( l = i -> ( F " ( l [,) +oo ) ) = ( F " ( i [,) +oo ) ) )
80 79 ineq1d 
 |-  ( l = i -> ( ( F " ( l [,) +oo ) ) i^i RR* ) = ( ( F " ( i [,) +oo ) ) i^i RR* ) )
81 80 supeq1d 
 |-  ( l = i -> sup ( ( ( F " ( l [,) +oo ) ) i^i RR* ) , RR* , < ) = sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) )
82 81 cbvmptv 
 |-  ( l e. RR |-> sup ( ( ( F " ( l [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) )
83 82 rneqi 
 |-  ran ( l e. RR |-> sup ( ( ( F " ( l [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ran ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) )
84 83 raleqi 
 |-  ( A. y e. ran ( l e. RR |-> sup ( ( ( F " ( l [,) +oo ) ) i^i RR* ) , RR* , < ) ) inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) <_ y <-> A. y e. ran ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) <_ y )
85 84 a1i 
 |-  ( ( ph /\ i e. RR ) -> ( A. y e. ran ( l e. RR |-> sup ( ( ( F " ( l [,) +oo ) ) i^i RR* ) , RR* , < ) ) inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) <_ y <-> A. y e. ran ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) <_ y ) )
86 77 85 mpbid 
 |-  ( ( ph /\ i e. RR ) -> A. y e. ran ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) <_ y )
87 supxrcl 
 |-  ( ( ( F " ( i [,) +oo ) ) i^i RR* ) C_ RR* -> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR* )
88 12 87 ax-mp 
 |-  sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR*
89 88 rgenw 
 |-  A. i e. RR sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR*
90 eqid 
 |-  ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) )
91 90 rnmptss 
 |-  ( A. i e. RR sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR* -> ran ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) C_ RR* )
92 89 91 ax-mp 
 |-  ran ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) C_ RR*
93 92 a1i 
 |-  ( ( ph /\ i e. RR ) -> ran ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) C_ RR* )
94 14 a1i 
 |-  ( ( ph /\ i e. RR ) -> inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR* )
95 infxrgelb 
 |-  ( ( ran ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) C_ RR* /\ inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR* ) -> ( inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) <_ inf ( ran ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) <-> A. y e. ran ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) <_ y ) )
96 93 94 95 syl2anc 
 |-  ( ( ph /\ i e. RR ) -> ( inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) <_ inf ( ran ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) <-> A. y e. ran ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) <_ y ) )
97 86 96 mpbird 
 |-  ( ( ph /\ i e. RR ) -> inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) <_ inf ( ran ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
98 97 ralrimiva 
 |-  ( ph -> A. i e. RR inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) <_ inf ( ran ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
99 nfv 
 |-  F/ i ph
100 nfcv 
 |-  F/_ i RR
101 nfmpt1 
 |-  F/_ i ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) )
102 101 nfrn 
 |-  F/_ i ran ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) )
103 nfcv 
 |-  F/_ i RR*
104 nfcv 
 |-  F/_ i <
105 102 103 104 nfinf 
 |-  F/_ i inf ( ran ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < )
106 infxrcl 
 |-  ( ran ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) C_ RR* -> inf ( ran ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) e. RR* )
107 92 106 ax-mp 
 |-  inf ( ran ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) e. RR*
108 107 a1i 
 |-  ( ph -> inf ( ran ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) e. RR* )
109 99 100 105 94 108 supxrleubrnmptf 
 |-  ( ph -> ( sup ( ran ( i e. RR |-> inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) <_ inf ( ran ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) <-> A. i e. RR inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) <_ inf ( ran ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) ) )
110 98 109 mpbird 
 |-  ( ph -> sup ( ran ( i e. RR |-> inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) <_ inf ( ran ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
111 eqid 
 |-  ( i e. RR |-> inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( i e. RR |-> inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) )
112 1 111 liminfvald 
 |-  ( ph -> ( liminf ` F ) = sup ( ran ( i e. RR |-> inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
113 1 90 limsupvald 
 |-  ( ph -> ( limsup ` F ) = inf ( ran ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
114 112 113 breq12d 
 |-  ( ph -> ( ( liminf ` F ) <_ ( limsup ` F ) <-> sup ( ran ( i e. RR |-> inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) <_ inf ( ran ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) ) )
115 110 114 mpbird 
 |-  ( ph -> ( liminf ` F ) <_ ( limsup ` F ) )