Metamath Proof Explorer

Theorem liminfval2

Description: The superior limit, relativized to an unbounded set. (Contributed by Glauco Siliprandi, 2-Jan-2022)

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

Proof

Step Hyp Ref Expression
1 liminfval2.1 
 |-  G = ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
2 liminfval2.2 
 |-  ( ph -> F e. V )
3 liminfval2.3 
 |-  ( ph -> A C_ RR )
4 liminfval2.4 
 |-  ( ph -> sup ( A , RR* , < ) = +oo )
5 oveq1 
 |-  ( k = j -> ( k [,) +oo ) = ( j [,) +oo ) )
6 5 imaeq2d 
 |-  ( k = j -> ( F " ( k [,) +oo ) ) = ( F " ( j [,) +oo ) ) )
7 6 ineq1d 
 |-  ( k = j -> ( ( F " ( k [,) +oo ) ) i^i RR* ) = ( ( F " ( j [,) +oo ) ) i^i RR* ) )
8 7 infeq1d 
 |-  ( k = j -> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) = inf ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) )
9 8 cbvmptv 
 |-  ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( j e. RR |-> inf ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) )
10 1 9 eqtri 
 |-  G = ( j e. RR |-> inf ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) )
11 10 liminfval 
 |-  ( F e. V -> ( liminf ` F ) = sup ( ran G , RR* , < ) )
12 2 11 syl 
 |-  ( ph -> ( liminf ` F ) = sup ( ran G , RR* , < ) )
13 3 ssrexr 
 |-  ( ph -> A C_ RR* )
14 supxrunb1 
 |-  ( A C_ RR* -> ( A. n e. RR E. x e. A n <_ x <-> sup ( A , RR* , < ) = +oo ) )
15 13 14 syl 
 |-  ( ph -> ( A. n e. RR E. x e. A n <_ x <-> sup ( A , RR* , < ) = +oo ) )
16 4 15 mpbird 
 |-  ( ph -> A. n e. RR E. x e. A n <_ x )
17 10 liminfgf 
 |-  G : RR --> RR*
18 17 ffvelcdmi 
 |-  ( n e. RR -> ( G ` n ) e. RR* )
19 18 ad2antlr 
 |-  ( ( ( ph /\ n e. RR ) /\ ( x e. A /\ n <_ x ) ) -> ( G ` n ) e. RR* )
20 simpll 
 |-  ( ( ( ph /\ n e. RR ) /\ ( x e. A /\ n <_ x ) ) -> ph )
21 simprl 
 |-  ( ( ( ph /\ n e. RR ) /\ ( x e. A /\ n <_ x ) ) -> x e. A )
22 3 sselda 
 |-  ( ( ph /\ x e. A ) -> x e. RR )
23 17 ffvelcdmi 
 |-  ( x e. RR -> ( G ` x ) e. RR* )
24 22 23 syl 
 |-  ( ( ph /\ x e. A ) -> ( G ` x ) e. RR* )
25 20 21 24 syl2anc 
 |-  ( ( ( ph /\ n e. RR ) /\ ( x e. A /\ n <_ x ) ) -> ( G ` x ) e. RR* )
26 imassrn 
 |-  ( G " A ) C_ ran G
27 frn 
 |-  ( G : RR --> RR* -> ran G C_ RR* )
28 17 27 ax-mp 
 |-  ran G C_ RR*
29 26 28 sstri 
 |-  ( G " A ) C_ RR*
30 supxrcl 
 |-  ( ( G " A ) C_ RR* -> sup ( ( G " A ) , RR* , < ) e. RR* )
31 29 30 ax-mp 
 |-  sup ( ( G " A ) , RR* , < ) e. RR*
32 31 a1i 
 |-  ( ( ( ph /\ n e. RR ) /\ ( x e. A /\ n <_ x ) ) -> sup ( ( G " A ) , RR* , < ) e. RR* )
33 simplr 
 |-  ( ( ( ph /\ n e. RR ) /\ ( x e. A /\ n <_ x ) ) -> n e. RR )
34 20 21 22 syl2anc 
 |-  ( ( ( ph /\ n e. RR ) /\ ( x e. A /\ n <_ x ) ) -> x e. RR )
35 simprr 
 |-  ( ( ( ph /\ n e. RR ) /\ ( x e. A /\ n <_ x ) ) -> n <_ x )
36 liminfgord 
 |-  ( ( n e. RR /\ x e. RR /\ n <_ x ) -> inf ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) <_ inf ( ( ( F " ( x [,) +oo ) ) i^i RR* ) , RR* , < ) )
37 33 34 35 36 syl3anc 
 |-  ( ( ( ph /\ n e. RR ) /\ ( x e. A /\ n <_ x ) ) -> inf ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) <_ inf ( ( ( F " ( x [,) +oo ) ) i^i RR* ) , RR* , < ) )
38 10 liminfgval 
 |-  ( n e. RR -> ( G ` n ) = inf ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) )
39 38 ad2antlr 
 |-  ( ( ( ph /\ n e. RR ) /\ x e. A ) -> ( G ` n ) = inf ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) )
40 10 liminfgval 
 |-  ( x e. RR -> ( G ` x ) = inf ( ( ( F " ( x [,) +oo ) ) i^i RR* ) , RR* , < ) )
41 22 40 syl 
 |-  ( ( ph /\ x e. A ) -> ( G ` x ) = inf ( ( ( F " ( x [,) +oo ) ) i^i RR* ) , RR* , < ) )
42 41 adantlr 
 |-  ( ( ( ph /\ n e. RR ) /\ x e. A ) -> ( G ` x ) = inf ( ( ( F " ( x [,) +oo ) ) i^i RR* ) , RR* , < ) )
43 39 42 breq12d 
 |-  ( ( ( ph /\ n e. RR ) /\ x e. A ) -> ( ( G ` n ) <_ ( G ` x ) <-> inf ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) <_ inf ( ( ( F " ( x [,) +oo ) ) i^i RR* ) , RR* , < ) ) )
44 43 adantrr 
 |-  ( ( ( ph /\ n e. RR ) /\ ( x e. A /\ n <_ x ) ) -> ( ( G ` n ) <_ ( G ` x ) <-> inf ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) <_ inf ( ( ( F " ( x [,) +oo ) ) i^i RR* ) , RR* , < ) ) )
45 37 44 mpbird 
 |-  ( ( ( ph /\ n e. RR ) /\ ( x e. A /\ n <_ x ) ) -> ( G ` n ) <_ ( G ` x ) )
46 29 a1i 
 |-  ( ( ph /\ x e. A ) -> ( G " A ) C_ RR* )
47 nfv 
 |-  F/ j ph
48 inss2 
 |-  ( ( F " ( j [,) +oo ) ) i^i RR* ) C_ RR*
49 infxrcl 
 |-  ( ( ( F " ( j [,) +oo ) ) i^i RR* ) C_ RR* -> inf ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR* )
50 48 49 ax-mp 
 |-  inf ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR*
51 50 a1i 
 |-  ( ( ph /\ j e. RR ) -> inf ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR* )
52 47 51 10 fnmptd 
 |-  ( ph -> G Fn RR )
53 52 adantr 
 |-  ( ( ph /\ x e. A ) -> G Fn RR )
54 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
55 53 22 54 fnfvimad 
 |-  ( ( ph /\ x e. A ) -> ( G ` x ) e. ( G " A ) )
56 supxrub 
 |-  ( ( ( G " A ) C_ RR* /\ ( G ` x ) e. ( G " A ) ) -> ( G ` x ) <_ sup ( ( G " A ) , RR* , < ) )
57 46 55 56 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( G ` x ) <_ sup ( ( G " A ) , RR* , < ) )
58 20 21 57 syl2anc 
 |-  ( ( ( ph /\ n e. RR ) /\ ( x e. A /\ n <_ x ) ) -> ( G ` x ) <_ sup ( ( G " A ) , RR* , < ) )
59 19 25 32 45 58 xrletrd 
 |-  ( ( ( ph /\ n e. RR ) /\ ( x e. A /\ n <_ x ) ) -> ( G ` n ) <_ sup ( ( G " A ) , RR* , < ) )
60 59 rexlimdvaa 
 |-  ( ( ph /\ n e. RR ) -> ( E. x e. A n <_ x -> ( G ` n ) <_ sup ( ( G " A ) , RR* , < ) ) )
61 60 ralimdva 
 |-  ( ph -> ( A. n e. RR E. x e. A n <_ x -> A. n e. RR ( G ` n ) <_ sup ( ( G " A ) , RR* , < ) ) )
62 16 61 mpd 
 |-  ( ph -> A. n e. RR ( G ` n ) <_ sup ( ( G " A ) , RR* , < ) )
63 xrltso 
 |-  < Or RR*
64 63 infex 
 |-  inf ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) e. _V
65 64 rgenw 
 |-  A. j e. RR inf ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) e. _V
66 10 fnmpt 
 |-  ( A. j e. RR inf ( ( ( F " ( j [,) +oo ) ) i^i RR* ) , RR* , < ) e. _V -> G Fn RR )
67 65 66 ax-mp 
 |-  G Fn RR
68 breq1 
 |-  ( x = ( G ` n ) -> ( x <_ sup ( ( G " A ) , RR* , < ) <-> ( G ` n ) <_ sup ( ( G " A ) , RR* , < ) ) )
69 68 ralrn 
 |-  ( G Fn RR -> ( A. x e. ran G x <_ sup ( ( G " A ) , RR* , < ) <-> A. n e. RR ( G ` n ) <_ sup ( ( G " A ) , RR* , < ) ) )
70 67 69 ax-mp 
 |-  ( A. x e. ran G x <_ sup ( ( G " A ) , RR* , < ) <-> A. n e. RR ( G ` n ) <_ sup ( ( G " A ) , RR* , < ) )
71 62 70 sylibr 
 |-  ( ph -> A. x e. ran G x <_ sup ( ( G " A ) , RR* , < ) )
72 supxrleub 
 |-  ( ( ran G C_ RR* /\ sup ( ( G " A ) , RR* , < ) e. RR* ) -> ( sup ( ran G , RR* , < ) <_ sup ( ( G " A ) , RR* , < ) <-> A. x e. ran G x <_ sup ( ( G " A ) , RR* , < ) ) )
73 28 31 72 mp2an 
 |-  ( sup ( ran G , RR* , < ) <_ sup ( ( G " A ) , RR* , < ) <-> A. x e. ran G x <_ sup ( ( G " A ) , RR* , < ) )
74 71 73 sylibr 
 |-  ( ph -> sup ( ran G , RR* , < ) <_ sup ( ( G " A ) , RR* , < ) )
75 26 a1i 
 |-  ( ph -> ( G " A ) C_ ran G )
76 28 a1i 
 |-  ( ph -> ran G C_ RR* )
77 supxrss 
 |-  ( ( ( G " A ) C_ ran G /\ ran G C_ RR* ) -> sup ( ( G " A ) , RR* , < ) <_ sup ( ran G , RR* , < ) )
78 75 76 77 syl2anc 
 |-  ( ph -> sup ( ( G " A ) , RR* , < ) <_ sup ( ran G , RR* , < ) )
79 supxrcl 
 |-  ( ran G C_ RR* -> sup ( ran G , RR* , < ) e. RR* )
80 28 79 ax-mp 
 |-  sup ( ran G , RR* , < ) e. RR*
81 xrletri3 
 |-  ( ( sup ( ran G , RR* , < ) e. RR* /\ sup ( ( G " A ) , RR* , < ) e. RR* ) -> ( sup ( ran G , RR* , < ) = sup ( ( G " A ) , RR* , < ) <-> ( sup ( ran G , RR* , < ) <_ sup ( ( G " A ) , RR* , < ) /\ sup ( ( G " A ) , RR* , < ) <_ sup ( ran G , RR* , < ) ) ) )
82 80 31 81 mp2an 
 |-  ( sup ( ran G , RR* , < ) = sup ( ( G " A ) , RR* , < ) <-> ( sup ( ran G , RR* , < ) <_ sup ( ( G " A ) , RR* , < ) /\ sup ( ( G " A ) , RR* , < ) <_ sup ( ran G , RR* , < ) ) )
83 74 78 82 sylanbrc 
 |-  ( ph -> sup ( ran G , RR* , < ) = sup ( ( G " A ) , RR* , < ) )
84 12 83 eqtrd 
 |-  ( ph -> ( liminf ` F ) = sup ( ( G " A ) , RR* , < ) )