Metamath Proof Explorer

Theorem limsupre3

Description: Given a function on the extended reals, its supremum limit is real if and only if two condition holds: 1. there is a real number that is less than or equal to the function, at some point, in any upper part of the reals; 2. there is a real number that is eventually greater than or equal to the function. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsupre3.1 
|- F/_ j F
limsupre3.2 
|- ( ph -> A C_ RR )
limsupre3.3 
|- ( ph -> F : A --> RR* )
Assertion limsupre3 
|- ( ph -> ( ( limsup ` F ) e. RR <-> ( E. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) /\ E. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) ) )

Proof

Step Hyp Ref Expression
1 limsupre3.1 
 |-  F/_ j F
2 limsupre3.2 
 |-  ( ph -> A C_ RR )
3 limsupre3.3 
 |-  ( ph -> F : A --> RR* )
4 nfcv 
 |-  F/_ l F
5 4 2 3 limsupre3lem 
 |-  ( ph -> ( ( limsup ` F ) e. RR <-> ( E. y e. RR A. i e. RR E. l e. A ( i <_ l /\ y <_ ( F ` l ) ) /\ E. y e. RR E. i e. RR A. l e. A ( i <_ l -> ( F ` l ) <_ y ) ) ) )
6 breq1 
 |-  ( y = x -> ( y <_ ( F ` l ) <-> x <_ ( F ` l ) ) )
7 6 anbi2d 
 |-  ( y = x -> ( ( i <_ l /\ y <_ ( F ` l ) ) <-> ( i <_ l /\ x <_ ( F ` l ) ) ) )
8 7 rexbidv 
 |-  ( y = x -> ( E. l e. A ( i <_ l /\ y <_ ( F ` l ) ) <-> E. l e. A ( i <_ l /\ x <_ ( F ` l ) ) ) )
9 8 ralbidv 
 |-  ( y = x -> ( A. i e. RR E. l e. A ( i <_ l /\ y <_ ( F ` l ) ) <-> A. i e. RR E. l e. A ( i <_ l /\ x <_ ( F ` l ) ) ) )
10 breq1 
 |-  ( i = k -> ( i <_ l <-> k <_ l ) )
11 10 anbi1d 
 |-  ( i = k -> ( ( i <_ l /\ x <_ ( F ` l ) ) <-> ( k <_ l /\ x <_ ( F ` l ) ) ) )
12 11 rexbidv 
 |-  ( i = k -> ( E. l e. A ( i <_ l /\ x <_ ( F ` l ) ) <-> E. l e. A ( k <_ l /\ x <_ ( F ` l ) ) ) )
13 nfv 
 |-  F/ j k <_ l
14 nfcv 
 |-  F/_ j x
15 nfcv 
 |-  F/_ j <_
16 nfcv 
 |-  F/_ j l
17 1 16 nffv 
 |-  F/_ j ( F ` l )
18 14 15 17 nfbr 
 |-  F/ j x <_ ( F ` l )
19 13 18 nfan 
 |-  F/ j ( k <_ l /\ x <_ ( F ` l ) )
20 nfv 
 |-  F/ l ( k <_ j /\ x <_ ( F ` j ) )
21 breq2 
 |-  ( l = j -> ( k <_ l <-> k <_ j ) )
22 fveq2 
 |-  ( l = j -> ( F ` l ) = ( F ` j ) )
23 22 breq2d 
 |-  ( l = j -> ( x <_ ( F ` l ) <-> x <_ ( F ` j ) ) )
24 21 23 anbi12d 
 |-  ( l = j -> ( ( k <_ l /\ x <_ ( F ` l ) ) <-> ( k <_ j /\ x <_ ( F ` j ) ) ) )
25 19 20 24 cbvrexw 
 |-  ( E. l e. A ( k <_ l /\ x <_ ( F ` l ) ) <-> E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) )
26 25 a1i 
 |-  ( i = k -> ( E. l e. A ( k <_ l /\ x <_ ( F ` l ) ) <-> E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) )
27 12 26 bitrd 
 |-  ( i = k -> ( E. l e. A ( i <_ l /\ x <_ ( F ` l ) ) <-> E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) )
28 27 cbvralvw 
 |-  ( A. i e. RR E. l e. A ( i <_ l /\ x <_ ( F ` l ) ) <-> A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) )
29 28 a1i 
 |-  ( y = x -> ( A. i e. RR E. l e. A ( i <_ l /\ x <_ ( F ` l ) ) <-> A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) )
30 9 29 bitrd 
 |-  ( y = x -> ( A. i e. RR E. l e. A ( i <_ l /\ y <_ ( F ` l ) ) <-> A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) )
31 30 cbvrexvw 
 |-  ( E. y e. RR A. i e. RR E. l e. A ( i <_ l /\ y <_ ( F ` l ) ) <-> E. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) )
32 breq2 
 |-  ( y = x -> ( ( F ` l ) <_ y <-> ( F ` l ) <_ x ) )
33 32 imbi2d 
 |-  ( y = x -> ( ( i <_ l -> ( F ` l ) <_ y ) <-> ( i <_ l -> ( F ` l ) <_ x ) ) )
34 33 ralbidv 
 |-  ( y = x -> ( A. l e. A ( i <_ l -> ( F ` l ) <_ y ) <-> A. l e. A ( i <_ l -> ( F ` l ) <_ x ) ) )
35 34 rexbidv 
 |-  ( y = x -> ( E. i e. RR A. l e. A ( i <_ l -> ( F ` l ) <_ y ) <-> E. i e. RR A. l e. A ( i <_ l -> ( F ` l ) <_ x ) ) )
36 10 imbi1d 
 |-  ( i = k -> ( ( i <_ l -> ( F ` l ) <_ x ) <-> ( k <_ l -> ( F ` l ) <_ x ) ) )
37 36 ralbidv 
 |-  ( i = k -> ( A. l e. A ( i <_ l -> ( F ` l ) <_ x ) <-> A. l e. A ( k <_ l -> ( F ` l ) <_ x ) ) )
38 17 15 14 nfbr 
 |-  F/ j ( F ` l ) <_ x
39 13 38 nfim 
 |-  F/ j ( k <_ l -> ( F ` l ) <_ x )
40 nfv 
 |-  F/ l ( k <_ j -> ( F ` j ) <_ x )
41 22 breq1d 
 |-  ( l = j -> ( ( F ` l ) <_ x <-> ( F ` j ) <_ x ) )
42 21 41 imbi12d 
 |-  ( l = j -> ( ( k <_ l -> ( F ` l ) <_ x ) <-> ( k <_ j -> ( F ` j ) <_ x ) ) )
43 39 40 42 cbvralw 
 |-  ( A. l e. A ( k <_ l -> ( F ` l ) <_ x ) <-> A. j e. A ( k <_ j -> ( F ` j ) <_ x ) )
44 43 a1i 
 |-  ( i = k -> ( A. l e. A ( k <_ l -> ( F ` l ) <_ x ) <-> A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) )
45 37 44 bitrd 
 |-  ( i = k -> ( A. l e. A ( i <_ l -> ( F ` l ) <_ x ) <-> A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) )
46 45 cbvrexvw 
 |-  ( E. i e. RR A. l e. A ( i <_ l -> ( F ` l ) <_ x ) <-> E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) )
47 46 a1i 
 |-  ( y = x -> ( E. i e. RR A. l e. A ( i <_ l -> ( F ` l ) <_ x ) <-> E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) )
48 35 47 bitrd 
 |-  ( y = x -> ( E. i e. RR A. l e. A ( i <_ l -> ( F ` l ) <_ y ) <-> E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) )
49 48 cbvrexvw 
 |-  ( E. y e. RR E. i e. RR A. l e. A ( i <_ l -> ( F ` l ) <_ y ) <-> E. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) )
50 31 49 anbi12i 
 |-  ( ( E. y e. RR A. i e. RR E. l e. A ( i <_ l /\ y <_ ( F ` l ) ) /\ E. y e. RR E. i e. RR A. l e. A ( i <_ l -> ( F ` l ) <_ y ) ) <-> ( E. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) /\ E. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) )
51 50 a1i 
 |-  ( ph -> ( ( E. y e. RR A. i e. RR E. l e. A ( i <_ l /\ y <_ ( F ` l ) ) /\ E. y e. RR E. i e. RR A. l e. A ( i <_ l -> ( F ` l ) <_ y ) ) <-> ( E. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) /\ E. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) ) )
52 5 51 bitrd 
 |-  ( ph -> ( ( limsup ` F ) e. RR <-> ( E. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) /\ E. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) ) )