Metamath Proof Explorer

Theorem limsupval2

Description: The superior limit, relativized to an unbounded set. (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by AV, 12-Sep-2020)

Ref Expression
Hypotheses limsupval.1 
|- G = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
limsupval2.1 
|- ( ph -> F e. V )
limsupval2.2 
|- ( ph -> A C_ RR )
limsupval2.3 
|- ( ph -> sup ( A , RR* , < ) = +oo )
Assertion limsupval2 
|- ( ph -> ( limsup ` F ) = inf ( ( G " A ) , RR* , < ) )

Proof

Step Hyp Ref Expression
1 limsupval.1 
 |-  G = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
2 limsupval2.1 
 |-  ( ph -> F e. V )
3 limsupval2.2 
 |-  ( ph -> A C_ RR )
4 limsupval2.3 
 |-  ( ph -> sup ( A , RR* , < ) = +oo )
5 1 limsupval 
 |-  ( F e. V -> ( limsup ` F ) = inf ( ran G , RR* , < ) )
6 2 5 syl 
 |-  ( ph -> ( limsup ` F ) = inf ( ran G , RR* , < ) )
7 imassrn 
 |-  ( G " A ) C_ ran G
8 1 limsupgf 
 |-  G : RR --> RR*
9 frn 
 |-  ( G : RR --> RR* -> ran G C_ RR* )
10 8 9 ax-mp 
 |-  ran G C_ RR*
11 infxrlb 
 |-  ( ( ran G C_ RR* /\ x e. ran G ) -> inf ( ran G , RR* , < ) <_ x )
12 11 ralrimiva 
 |-  ( ran G C_ RR* -> A. x e. ran G inf ( ran G , RR* , < ) <_ x )
13 10 12 mp1i 
 |-  ( ph -> A. x e. ran G inf ( ran G , RR* , < ) <_ x )
14 ssralv 
 |-  ( ( G " A ) C_ ran G -> ( A. x e. ran G inf ( ran G , RR* , < ) <_ x -> A. x e. ( G " A ) inf ( ran G , RR* , < ) <_ x ) )
15 7 13 14 mpsyl 
 |-  ( ph -> A. x e. ( G " A ) inf ( ran G , RR* , < ) <_ x )
16 7 10 sstri 
 |-  ( G " A ) C_ RR*
17 infxrcl 
 |-  ( ran G C_ RR* -> inf ( ran G , RR* , < ) e. RR* )
18 10 17 ax-mp 
 |-  inf ( ran G , RR* , < ) e. RR*
19 infxrgelb 
 |-  ( ( ( G " A ) C_ RR* /\ inf ( ran G , RR* , < ) e. RR* ) -> ( inf ( ran G , RR* , < ) <_ inf ( ( G " A ) , RR* , < ) <-> A. x e. ( G " A ) inf ( ran G , RR* , < ) <_ x ) )
20 16 18 19 mp2an 
 |-  ( inf ( ran G , RR* , < ) <_ inf ( ( G " A ) , RR* , < ) <-> A. x e. ( G " A ) inf ( ran G , RR* , < ) <_ x )
21 15 20 sylibr 
 |-  ( ph -> inf ( ran G , RR* , < ) <_ inf ( ( G " A ) , RR* , < ) )
22 ressxr 
 |-  RR C_ RR*
23 3 22 sstrdi 
 |-  ( ph -> A C_ RR* )
24 supxrunb1 
 |-  ( A C_ RR* -> ( A. n e. RR E. x e. A n <_ x <-> sup ( A , RR* , < ) = +oo ) )
25 23 24 syl 
 |-  ( ph -> ( A. n e. RR E. x e. A n <_ x <-> sup ( A , RR* , < ) = +oo ) )
26 4 25 mpbird 
 |-  ( ph -> A. n e. RR E. x e. A n <_ x )
27 infxrcl 
 |-  ( ( G " A ) C_ RR* -> inf ( ( G " A ) , RR* , < ) e. RR* )
28 16 27 mp1i 
 |-  ( ( ( ph /\ n e. RR ) /\ ( x e. A /\ n <_ x ) ) -> inf ( ( G " A ) , RR* , < ) e. RR* )
29 3 sselda 
 |-  ( ( ph /\ x e. A ) -> x e. RR )
30 29 ad2ant2r 
 |-  ( ( ( ph /\ n e. RR ) /\ ( x e. A /\ n <_ x ) ) -> x e. RR )
31 8 ffvelcdmi 
 |-  ( x e. RR -> ( G ` x ) e. RR* )
32 30 31 syl 
 |-  ( ( ( ph /\ n e. RR ) /\ ( x e. A /\ n <_ x ) ) -> ( G ` x ) e. RR* )
33 8 ffvelcdmi 
 |-  ( n e. RR -> ( G ` n ) e. RR* )
34 33 ad2antlr 
 |-  ( ( ( ph /\ n e. RR ) /\ ( x e. A /\ n <_ x ) ) -> ( G ` n ) e. RR* )
35 ffn 
 |-  ( G : RR --> RR* -> G Fn RR )
36 8 35 mp1i 
 |-  ( ( ( ph /\ n e. RR ) /\ ( x e. A /\ n <_ x ) ) -> G Fn RR )
37 3 ad2antrr 
 |-  ( ( ( ph /\ n e. RR ) /\ ( x e. A /\ n <_ x ) ) -> A C_ RR )
38 simprl 
 |-  ( ( ( ph /\ n e. RR ) /\ ( x e. A /\ n <_ x ) ) -> x e. A )
39 fnfvima 
 |-  ( ( G Fn RR /\ A C_ RR /\ x e. A ) -> ( G ` x ) e. ( G " A ) )
40 36 37 38 39 syl3anc 
 |-  ( ( ( ph /\ n e. RR ) /\ ( x e. A /\ n <_ x ) ) -> ( G ` x ) e. ( G " A ) )
41 infxrlb 
 |-  ( ( ( G " A ) C_ RR* /\ ( G ` x ) e. ( G " A ) ) -> inf ( ( G " A ) , RR* , < ) <_ ( G ` x ) )
42 16 40 41 sylancr 
 |-  ( ( ( ph /\ n e. RR ) /\ ( x e. A /\ n <_ x ) ) -> inf ( ( G " A ) , RR* , < ) <_ ( G ` x ) )
43 simplr 
 |-  ( ( ( ph /\ n e. RR ) /\ ( x e. A /\ n <_ x ) ) -> n e. RR )
44 simprr 
 |-  ( ( ( ph /\ n e. RR ) /\ ( x e. A /\ n <_ x ) ) -> n <_ x )
45 limsupgord 
 |-  ( ( n e. RR /\ x e. RR /\ n <_ x ) -> sup ( ( ( F " ( x [,) +oo ) ) i^i RR* ) , RR* , < ) <_ sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) )
46 43 30 44 45 syl3anc 
 |-  ( ( ( ph /\ n e. RR ) /\ ( x e. A /\ n <_ x ) ) -> sup ( ( ( F " ( x [,) +oo ) ) i^i RR* ) , RR* , < ) <_ sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) )
47 1 limsupgval 
 |-  ( x e. RR -> ( G ` x ) = sup ( ( ( F " ( x [,) +oo ) ) i^i RR* ) , RR* , < ) )
48 30 47 syl 
 |-  ( ( ( ph /\ n e. RR ) /\ ( x e. A /\ n <_ x ) ) -> ( G ` x ) = sup ( ( ( F " ( x [,) +oo ) ) i^i RR* ) , RR* , < ) )
49 1 limsupgval 
 |-  ( n e. RR -> ( G ` n ) = sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) )
50 49 ad2antlr 
 |-  ( ( ( ph /\ n e. RR ) /\ ( x e. A /\ n <_ x ) ) -> ( G ` n ) = sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) )
51 46 48 50 3brtr4d 
 |-  ( ( ( ph /\ n e. RR ) /\ ( x e. A /\ n <_ x ) ) -> ( G ` x ) <_ ( G ` n ) )
52 28 32 34 42 51 xrletrd 
 |-  ( ( ( ph /\ n e. RR ) /\ ( x e. A /\ n <_ x ) ) -> inf ( ( G " A ) , RR* , < ) <_ ( G ` n ) )
53 52 rexlimdvaa 
 |-  ( ( ph /\ n e. RR ) -> ( E. x e. A n <_ x -> inf ( ( G " A ) , RR* , < ) <_ ( G ` n ) ) )
54 53 ralimdva 
 |-  ( ph -> ( A. n e. RR E. x e. A n <_ x -> A. n e. RR inf ( ( G " A ) , RR* , < ) <_ ( G ` n ) ) )
55 26 54 mpd 
 |-  ( ph -> A. n e. RR inf ( ( G " A ) , RR* , < ) <_ ( G ` n ) )
56 8 35 ax-mp 
 |-  G Fn RR
57 breq2 
 |-  ( x = ( G ` n ) -> ( inf ( ( G " A ) , RR* , < ) <_ x <-> inf ( ( G " A ) , RR* , < ) <_ ( G ` n ) ) )
58 57 ralrn 
 |-  ( G Fn RR -> ( A. x e. ran G inf ( ( G " A ) , RR* , < ) <_ x <-> A. n e. RR inf ( ( G " A ) , RR* , < ) <_ ( G ` n ) ) )
59 56 58 ax-mp 
 |-  ( A. x e. ran G inf ( ( G " A ) , RR* , < ) <_ x <-> A. n e. RR inf ( ( G " A ) , RR* , < ) <_ ( G ` n ) )
60 55 59 sylibr 
 |-  ( ph -> A. x e. ran G inf ( ( G " A ) , RR* , < ) <_ x )
61 16 27 ax-mp 
 |-  inf ( ( G " A ) , RR* , < ) e. RR*
62 infxrgelb 
 |-  ( ( ran G C_ RR* /\ inf ( ( G " A ) , RR* , < ) e. RR* ) -> ( inf ( ( G " A ) , RR* , < ) <_ inf ( ran G , RR* , < ) <-> A. x e. ran G inf ( ( G " A ) , RR* , < ) <_ x ) )
63 10 61 62 mp2an 
 |-  ( inf ( ( G " A ) , RR* , < ) <_ inf ( ran G , RR* , < ) <-> A. x e. ran G inf ( ( G " A ) , RR* , < ) <_ x )
64 60 63 sylibr 
 |-  ( ph -> inf ( ( G " A ) , RR* , < ) <_ inf ( ran G , RR* , < ) )
65 xrletri3 
 |-  ( ( inf ( ran G , RR* , < ) e. RR* /\ inf ( ( G " A ) , RR* , < ) e. RR* ) -> ( inf ( ran G , RR* , < ) = inf ( ( G " A ) , RR* , < ) <-> ( inf ( ran G , RR* , < ) <_ inf ( ( G " A ) , RR* , < ) /\ inf ( ( G " A ) , RR* , < ) <_ inf ( ran G , RR* , < ) ) ) )
66 18 61 65 mp2an 
 |-  ( inf ( ran G , RR* , < ) = inf ( ( G " A ) , RR* , < ) <-> ( inf ( ran G , RR* , < ) <_ inf ( ( G " A ) , RR* , < ) /\ inf ( ( G " A ) , RR* , < ) <_ inf ( ran G , RR* , < ) ) )
67 21 64 66 sylanbrc 
 |-  ( ph -> inf ( ran G , RR* , < ) = inf ( ( G " A ) , RR* , < ) )
68 6 67 eqtrd 
 |-  ( ph -> ( limsup ` F ) = inf ( ( G " A ) , RR* , < ) )