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 inss2 
 |-  ( ( F " ( i [,) +oo ) ) i^i RR* ) C_ RR*
4 infxrcl 
 |-  ( ( ( F " ( i [,) +oo ) ) i^i RR* ) C_ RR* -> inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR* )
5 3 4 ax-mp 
 |-  inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR*
6 5 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* )
7 inss2 
 |-  ( ( F " ( j [,) +oo ) ) i^i RR* ) C_ RR*
8 infxrcl 
 |-  ( ( ( F " ( j [,) +oo ) ) i^i RR* ) C_ RR* -> inf ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR* )
9 7 8 ax-mp 
 |-  inf ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR*
10 9 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* )
11 inss2 
 |-  ( ( F " ( l [,) +oo ) ) i^i RR* ) C_ RR*
12 11 supxrcli 
 |-  sup ( ( ( F " ( l [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR*
13 12 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* )
14 rexr 
 |-  ( i e. RR -> i e. RR* )
15 14 ad2antrr 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> i e. RR* )
16 pnfxr 
 |-  +oo e. RR*
17 16 a1i 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> +oo e. RR* )
18 simpr 
 |-  ( ( i e. RR /\ l e. RR ) -> l e. RR )
19 simpl 
 |-  ( ( i e. RR /\ l e. RR ) -> i e. RR )
20 18 19 ifcld 
 |-  ( ( i e. RR /\ l e. RR ) -> if ( i <_ l , l , i ) e. RR )
21 20 rexrd 
 |-  ( ( i e. RR /\ l e. RR ) -> if ( i <_ l , l , i ) e. RR* )
22 21 adantr 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> if ( i <_ l , l , i ) e. RR* )
23 icossxr 
 |-  ( if ( i <_ l , l , i ) [,) +oo ) C_ RR*
24 23 sseli 
 |-  ( j e. ( if ( i <_ l , l , i ) [,) +oo ) -> j e. RR* )
25 24 adantl 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> j e. RR* )
26 max1 
 |-  ( ( i e. RR /\ l e. RR ) -> i <_ if ( i <_ l , l , i ) )
27 26 adantr 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> i <_ if ( i <_ l , l , i ) )
28 simpr 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> j e. ( if ( i <_ l , l , i ) [,) +oo ) )
29 22 17 28 icogelbd 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> if ( i <_ l , l , i ) <_ j )
30 15 22 25 27 29 xrletrd 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> i <_ j )
31 15 17 30 icossico2d 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> ( j [,) +oo ) C_ ( i [,) +oo ) )
32 31 imass2d 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> ( F " ( j [,) +oo ) ) C_ ( F " ( i [,) +oo ) ) )
33 32 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* ) )
34 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* , < ) )
35 33 3 34 sylancl 
 |-  ( ( ( 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* , < ) )
36 35 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* , < ) )
37 7 supxrcli 
 |-  sup ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR*
38 37 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* )
39 7 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* )
40 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* ) =/= (/) )
41 39 40 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* , < ) )
42 rexr 
 |-  ( l e. RR -> l e. RR* )
43 42 ad2antlr 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> l e. RR* )
44 max2 
 |-  ( ( i e. RR /\ l e. RR ) -> l <_ if ( i <_ l , l , i ) )
45 44 adantr 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> l <_ if ( i <_ l , l , i ) )
46 43 22 25 45 29 xrletrd 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> l <_ j )
47 43 17 46 icossico2d 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> ( j [,) +oo ) C_ ( l [,) +oo ) )
48 47 imass2d 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> ( F " ( j [,) +oo ) ) C_ ( F " ( l [,) +oo ) ) )
49 48 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* ) )
50 11 a1i 
 |-  ( ( ( i e. RR /\ l e. RR ) /\ j e. ( if ( i <_ l , l , i ) [,) +oo ) ) -> ( ( F " ( l [,) +oo ) ) i^i RR* ) C_ RR* )
51 49 50 xrsupssd 
 |-  ( ( ( 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* , < ) )
52 51 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* , < ) )
53 10 38 13 41 52 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* , < ) )
54 6 10 13 36 53 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* , < ) )
55 54 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* , < ) )
56 oveq1 
 |-  ( k = if ( i <_ l , l , i ) -> ( k [,) +oo ) = ( if ( i <_ l , l , i ) [,) +oo ) )
57 56 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* ) =/= (/) ) )
58 2 ad2antrr 
 |-  ( ( ( ph /\ i e. RR ) /\ l e. RR ) -> A. k e. RR E. j e. ( k [,) +oo ) ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) )
59 20 adantll 
 |-  ( ( ( ph /\ i e. RR ) /\ l e. RR ) -> if ( i <_ l , l , i ) e. RR )
60 57 58 59 rspcdva 
 |-  ( ( ( ph /\ i e. RR ) /\ l e. RR ) -> E. j e. ( if ( i <_ l , l , i ) [,) +oo ) ( ( F " ( j [,) +oo ) ) i^i RR* ) =/= (/) )
61 55 60 r19.29a 
 |-  ( ( ( ph /\ i e. RR ) /\ l e. RR ) -> inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) <_ sup ( ( ( F " ( l [,) +oo ) ) i^i RR* ) , RR* , < ) )
62 61 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* , < ) )
63 nfv 
 |-  F/ l ph
64 xrltso 
 |-  < Or RR*
65 64 supex 
 |-  sup ( ( ( F " ( l [,) +oo ) ) i^i RR* ) , RR* , < ) e. _V
66 65 a1i 
 |-  ( ( ph /\ l e. RR ) -> sup ( ( ( F " ( l [,) +oo ) ) i^i RR* ) , RR* , < ) e. _V )
67 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* , < ) ) )
68 63 66 67 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* , < ) ) )
69 68 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* , < ) ) )
70 62 69 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 )
71 oveq1 
 |-  ( l = i -> ( l [,) +oo ) = ( i [,) +oo ) )
72 71 imaeq2d 
 |-  ( l = i -> ( F " ( l [,) +oo ) ) = ( F " ( i [,) +oo ) ) )
73 72 ineq1d 
 |-  ( l = i -> ( ( F " ( l [,) +oo ) ) i^i RR* ) = ( ( F " ( i [,) +oo ) ) i^i RR* ) )
74 73 supeq1d 
 |-  ( l = i -> sup ( ( ( F " ( l [,) +oo ) ) i^i RR* ) , RR* , < ) = sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) )
75 74 cbvmptv 
 |-  ( l e. RR |-> sup ( ( ( F " ( l [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) )
76 75 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* , < ) )
77 76 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 )
78 70 77 sylib 
 |-  ( ( 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 )
79 3 supxrcli 
 |-  sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR*
80 79 rgenw 
 |-  A. i e. RR sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR*
81 eqid 
 |-  ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) )
82 81 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* )
83 80 82 ax-mp 
 |-  ran ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) C_ RR*
84 83 a1i 
 |-  ( ( ph /\ i e. RR ) -> ran ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) C_ RR* )
85 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 ) )
86 84 5 85 sylancl 
 |-  ( ( 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 ) )
87 78 86 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* , < ) )
88 87 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* , < ) )
89 nfv 
 |-  F/ i ph
90 nfcv 
 |-  F/_ i RR
91 nfmpt1 
 |-  F/_ i ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) )
92 91 nfrn 
 |-  F/_ i ran ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) )
93 nfcv 
 |-  F/_ i RR*
94 nfcv 
 |-  F/_ i <
95 92 93 94 nfinf 
 |-  F/_ i inf ( ran ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < )
96 5 a1i 
 |-  ( ( ph /\ i e. RR ) -> inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR* )
97 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* )
98 83 97 ax-mp 
 |-  inf ( ran ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) e. RR*
99 98 a1i 
 |-  ( ph -> inf ( ran ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) e. RR* )
100 89 90 95 96 99 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* , < ) ) )
101 88 100 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* , < ) )
102 eqid 
 |-  ( i e. RR |-> inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( i e. RR |-> inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) )
103 1 102 liminfvald 
 |-  ( ph -> ( liminf ` F ) = sup ( ran ( i e. RR |-> inf ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
104 1 81 limsupvald 
 |-  ( ph -> ( limsup ` F ) = inf ( ran ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
105 101 103 104 3brtr4d 
 |-  ( ph -> ( liminf ` F ) <_ ( limsup ` F ) )