Metamath Proof Explorer

Theorem limsupre3mpt

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 limsupre3mpt.p 
|- F/ x ph
limsupre3mpt.a 
|- ( ph -> A C_ RR )
limsupre3mpt.b 
|- ( ( ph /\ x e. A ) -> B e. RR* )
Assertion limsupre3mpt 
|- ( ph -> ( ( limsup ` ( x e. A |-> B ) ) e. RR <-> ( E. y e. RR A. k e. RR E. x e. A ( k <_ x /\ y <_ B ) /\ E. y e. RR E. k e. RR A. x e. A ( k <_ x -> B <_ y ) ) ) )

Proof

Step Hyp Ref Expression
1 limsupre3mpt.p 
 |-  F/ x ph
2 limsupre3mpt.a 
 |-  ( ph -> A C_ RR )
3 limsupre3mpt.b 
 |-  ( ( ph /\ x e. A ) -> B e. RR* )
4 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
5 1 3 fmptd2f 
 |-  ( ph -> ( x e. A |-> B ) : A --> RR* )
6 4 2 5 limsupre3 
 |-  ( ph -> ( ( limsup ` ( x e. A |-> B ) ) e. RR <-> ( E. w e. RR A. j e. RR E. x e. A ( j <_ x /\ w <_ ( ( x e. A |-> B ) ` x ) ) /\ E. w e. RR E. j e. RR A. x e. A ( j <_ x -> ( ( x e. A |-> B ) ` x ) <_ w ) ) ) )
7 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
8 7 a1i 
 |-  ( ph -> ( x e. A |-> B ) = ( x e. A |-> B ) )
9 8 3 fvmpt2d 
 |-  ( ( ph /\ x e. A ) -> ( ( x e. A |-> B ) ` x ) = B )
10 9 breq2d 
 |-  ( ( ph /\ x e. A ) -> ( w <_ ( ( x e. A |-> B ) ` x ) <-> w <_ B ) )
11 10 anbi2d 
 |-  ( ( ph /\ x e. A ) -> ( ( j <_ x /\ w <_ ( ( x e. A |-> B ) ` x ) ) <-> ( j <_ x /\ w <_ B ) ) )
12 1 11 rexbida 
 |-  ( ph -> ( E. x e. A ( j <_ x /\ w <_ ( ( x e. A |-> B ) ` x ) ) <-> E. x e. A ( j <_ x /\ w <_ B ) ) )
13 12 ralbidv 
 |-  ( ph -> ( A. j e. RR E. x e. A ( j <_ x /\ w <_ ( ( x e. A |-> B ) ` x ) ) <-> A. j e. RR E. x e. A ( j <_ x /\ w <_ B ) ) )
14 13 rexbidv 
 |-  ( ph -> ( E. w e. RR A. j e. RR E. x e. A ( j <_ x /\ w <_ ( ( x e. A |-> B ) ` x ) ) <-> E. w e. RR A. j e. RR E. x e. A ( j <_ x /\ w <_ B ) ) )
15 9 breq1d 
 |-  ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> B ) ` x ) <_ w <-> B <_ w ) )
16 15 imbi2d 
 |-  ( ( ph /\ x e. A ) -> ( ( j <_ x -> ( ( x e. A |-> B ) ` x ) <_ w ) <-> ( j <_ x -> B <_ w ) ) )
17 1 16 ralbida 
 |-  ( ph -> ( A. x e. A ( j <_ x -> ( ( x e. A |-> B ) ` x ) <_ w ) <-> A. x e. A ( j <_ x -> B <_ w ) ) )
18 17 rexbidv 
 |-  ( ph -> ( E. j e. RR A. x e. A ( j <_ x -> ( ( x e. A |-> B ) ` x ) <_ w ) <-> E. j e. RR A. x e. A ( j <_ x -> B <_ w ) ) )
19 18 rexbidv 
 |-  ( ph -> ( E. w e. RR E. j e. RR A. x e. A ( j <_ x -> ( ( x e. A |-> B ) ` x ) <_ w ) <-> E. w e. RR E. j e. RR A. x e. A ( j <_ x -> B <_ w ) ) )
20 14 19 anbi12d 
 |-  ( ph -> ( ( E. w e. RR A. j e. RR E. x e. A ( j <_ x /\ w <_ ( ( x e. A |-> B ) ` x ) ) /\ E. w e. RR E. j e. RR A. x e. A ( j <_ x -> ( ( x e. A |-> B ) ` x ) <_ w ) ) <-> ( E. w e. RR A. j e. RR E. x e. A ( j <_ x /\ w <_ B ) /\ E. w e. RR E. j e. RR A. x e. A ( j <_ x -> B <_ w ) ) ) )
21 breq1 
 |-  ( w = y -> ( w <_ B <-> y <_ B ) )
22 21 anbi2d 
 |-  ( w = y -> ( ( j <_ x /\ w <_ B ) <-> ( j <_ x /\ y <_ B ) ) )
23 22 rexbidv 
 |-  ( w = y -> ( E. x e. A ( j <_ x /\ w <_ B ) <-> E. x e. A ( j <_ x /\ y <_ B ) ) )
24 23 ralbidv 
 |-  ( w = y -> ( A. j e. RR E. x e. A ( j <_ x /\ w <_ B ) <-> A. j e. RR E. x e. A ( j <_ x /\ y <_ B ) ) )
25 breq1 
 |-  ( j = k -> ( j <_ x <-> k <_ x ) )
26 25 anbi1d 
 |-  ( j = k -> ( ( j <_ x /\ y <_ B ) <-> ( k <_ x /\ y <_ B ) ) )
27 26 rexbidv 
 |-  ( j = k -> ( E. x e. A ( j <_ x /\ y <_ B ) <-> E. x e. A ( k <_ x /\ y <_ B ) ) )
28 27 cbvralvw 
 |-  ( A. j e. RR E. x e. A ( j <_ x /\ y <_ B ) <-> A. k e. RR E. x e. A ( k <_ x /\ y <_ B ) )
29 28 a1i 
 |-  ( w = y -> ( A. j e. RR E. x e. A ( j <_ x /\ y <_ B ) <-> A. k e. RR E. x e. A ( k <_ x /\ y <_ B ) ) )
30 24 29 bitrd 
 |-  ( w = y -> ( A. j e. RR E. x e. A ( j <_ x /\ w <_ B ) <-> A. k e. RR E. x e. A ( k <_ x /\ y <_ B ) ) )
31 30 cbvrexvw 
 |-  ( E. w e. RR A. j e. RR E. x e. A ( j <_ x /\ w <_ B ) <-> E. y e. RR A. k e. RR E. x e. A ( k <_ x /\ y <_ B ) )
32 breq2 
 |-  ( w = y -> ( B <_ w <-> B <_ y ) )
33 32 imbi2d 
 |-  ( w = y -> ( ( j <_ x -> B <_ w ) <-> ( j <_ x -> B <_ y ) ) )
34 33 ralbidv 
 |-  ( w = y -> ( A. x e. A ( j <_ x -> B <_ w ) <-> A. x e. A ( j <_ x -> B <_ y ) ) )
35 34 rexbidv 
 |-  ( w = y -> ( E. j e. RR A. x e. A ( j <_ x -> B <_ w ) <-> E. j e. RR A. x e. A ( j <_ x -> B <_ y ) ) )
36 25 imbi1d 
 |-  ( j = k -> ( ( j <_ x -> B <_ y ) <-> ( k <_ x -> B <_ y ) ) )
37 36 ralbidv 
 |-  ( j = k -> ( A. x e. A ( j <_ x -> B <_ y ) <-> A. x e. A ( k <_ x -> B <_ y ) ) )
38 37 cbvrexvw 
 |-  ( E. j e. RR A. x e. A ( j <_ x -> B <_ y ) <-> E. k e. RR A. x e. A ( k <_ x -> B <_ y ) )
39 38 a1i 
 |-  ( w = y -> ( E. j e. RR A. x e. A ( j <_ x -> B <_ y ) <-> E. k e. RR A. x e. A ( k <_ x -> B <_ y ) ) )
40 35 39 bitrd 
 |-  ( w = y -> ( E. j e. RR A. x e. A ( j <_ x -> B <_ w ) <-> E. k e. RR A. x e. A ( k <_ x -> B <_ y ) ) )
41 40 cbvrexvw 
 |-  ( E. w e. RR E. j e. RR A. x e. A ( j <_ x -> B <_ w ) <-> E. y e. RR E. k e. RR A. x e. A ( k <_ x -> B <_ y ) )
42 31 41 anbi12i 
 |-  ( ( E. w e. RR A. j e. RR E. x e. A ( j <_ x /\ w <_ B ) /\ E. w e. RR E. j e. RR A. x e. A ( j <_ x -> B <_ w ) ) <-> ( E. y e. RR A. k e. RR E. x e. A ( k <_ x /\ y <_ B ) /\ E. y e. RR E. k e. RR A. x e. A ( k <_ x -> B <_ y ) ) )
43 42 a1i 
 |-  ( ph -> ( ( E. w e. RR A. j e. RR E. x e. A ( j <_ x /\ w <_ B ) /\ E. w e. RR E. j e. RR A. x e. A ( j <_ x -> B <_ w ) ) <-> ( E. y e. RR A. k e. RR E. x e. A ( k <_ x /\ y <_ B ) /\ E. y e. RR E. k e. RR A. x e. A ( k <_ x -> B <_ y ) ) ) )
44 6 20 43 3bitrd 
 |-  ( ph -> ( ( limsup ` ( x e. A |-> B ) ) e. RR <-> ( E. y e. RR A. k e. RR E. x e. A ( k <_ x /\ y <_ B ) /\ E. y e. RR E. k e. RR A. x e. A ( k <_ x -> B <_ y ) ) ) )