Metamath Proof Explorer

Theorem liminfresico

Description: The inferior limit doesn't change when a function is restricted to an upperset of reals. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses liminfresico.1 
|- ( ph -> M e. RR )
liminfresico.2 
|- Z = ( M [,) +oo )
liminfresico.3 
|- ( ph -> F e. V )
Assertion liminfresico 
|- ( ph -> ( liminf ` ( F |` Z ) ) = ( liminf ` F ) )

Proof

Step Hyp Ref Expression
1 liminfresico.1 
 |-  ( ph -> M e. RR )
2 liminfresico.2 
 |-  Z = ( M [,) +oo )
3 liminfresico.3 
 |-  ( ph -> F e. V )
4 1 rexrd 
 |-  ( ph -> M e. RR* )
5 4 ad2antrr 
 |-  ( ( ( ph /\ k e. Z ) /\ y e. ( k [,) +oo ) ) -> M e. RR* )
6 pnfxr 
 |-  +oo e. RR*
7 6 a1i 
 |-  ( ( ( ph /\ k e. Z ) /\ y e. ( k [,) +oo ) ) -> +oo e. RR* )
8 ressxr 
 |-  RR C_ RR*
9 6 a1i 
 |-  ( ph -> +oo e. RR* )
10 icossre 
 |-  ( ( M e. RR /\ +oo e. RR* ) -> ( M [,) +oo ) C_ RR )
11 1 9 10 syl2anc 
 |-  ( ph -> ( M [,) +oo ) C_ RR )
12 11 adantr 
 |-  ( ( ph /\ k e. Z ) -> ( M [,) +oo ) C_ RR )
13 2 eleq2i 
 |-  ( k e. Z <-> k e. ( M [,) +oo ) )
14 13 bilani 
 |-  ( ( ph /\ k e. Z ) -> k e. ( M [,) +oo ) )
15 12 14 sseldd 
 |-  ( ( ph /\ k e. Z ) -> k e. RR )
16 15 adantr 
 |-  ( ( ( ph /\ k e. Z ) /\ y e. ( k [,) +oo ) ) -> k e. RR )
17 simpr 
 |-  ( ( ( ph /\ k e. Z ) /\ y e. ( k [,) +oo ) ) -> y e. ( k [,) +oo ) )
18 elicore 
 |-  ( ( k e. RR /\ y e. ( k [,) +oo ) ) -> y e. RR )
19 16 17 18 syl2anc 
 |-  ( ( ( ph /\ k e. Z ) /\ y e. ( k [,) +oo ) ) -> y e. RR )
20 8 19 sselid 
 |-  ( ( ( ph /\ k e. Z ) /\ y e. ( k [,) +oo ) ) -> y e. RR* )
21 1 ad2antrr 
 |-  ( ( ( ph /\ k e. Z ) /\ y e. ( k [,) +oo ) ) -> M e. RR )
22 4 adantr 
 |-  ( ( ph /\ k e. Z ) -> M e. RR* )
23 6 a1i 
 |-  ( ( ph /\ k e. Z ) -> +oo e. RR* )
24 22 23 14 icogelbd 
 |-  ( ( ph /\ k e. Z ) -> M <_ k )
25 24 adantr 
 |-  ( ( ( ph /\ k e. Z ) /\ y e. ( k [,) +oo ) ) -> M <_ k )
26 8 16 sselid 
 |-  ( ( ( ph /\ k e. Z ) /\ y e. ( k [,) +oo ) ) -> k e. RR* )
27 26 7 17 icogelbd 
 |-  ( ( ( ph /\ k e. Z ) /\ y e. ( k [,) +oo ) ) -> k <_ y )
28 21 16 19 25 27 letrd 
 |-  ( ( ( ph /\ k e. Z ) /\ y e. ( k [,) +oo ) ) -> M <_ y )
29 19 ltpnfd 
 |-  ( ( ( ph /\ k e. Z ) /\ y e. ( k [,) +oo ) ) -> y < +oo )
30 5 7 20 28 29 elicod 
 |-  ( ( ( ph /\ k e. Z ) /\ y e. ( k [,) +oo ) ) -> y e. ( M [,) +oo ) )
31 30 2 eleqtrrdi 
 |-  ( ( ( ph /\ k e. Z ) /\ y e. ( k [,) +oo ) ) -> y e. Z )
32 31 ssd 
 |-  ( ( ph /\ k e. Z ) -> ( k [,) +oo ) C_ Z )
33 resima2 
 |-  ( ( k [,) +oo ) C_ Z -> ( ( F |` Z ) " ( k [,) +oo ) ) = ( F " ( k [,) +oo ) ) )
34 32 33 syl 
 |-  ( ( ph /\ k e. Z ) -> ( ( F |` Z ) " ( k [,) +oo ) ) = ( F " ( k [,) +oo ) ) )
35 34 ineq1d 
 |-  ( ( ph /\ k e. Z ) -> ( ( ( F |` Z ) " ( k [,) +oo ) ) i^i RR* ) = ( ( F " ( k [,) +oo ) ) i^i RR* ) )
36 35 infeq1d 
 |-  ( ( ph /\ k e. Z ) -> inf ( ( ( ( F |` Z ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) = inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
37 36 mpteq2dva 
 |-  ( ph -> ( k e. Z |-> inf ( ( ( ( F |` Z ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( k e. Z |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) )
38 37 rneqd 
 |-  ( ph -> ran ( k e. Z |-> inf ( ( ( ( F |` Z ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ran ( k e. Z |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) )
39 2 11 eqsstrid 
 |-  ( ph -> Z C_ RR )
40 39 mptimass 
 |-  ( ph -> ( ( k e. RR |-> inf ( ( ( ( F |` Z ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) " Z ) = ran ( k e. Z |-> inf ( ( ( ( F |` Z ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) )
41 39 mptimass 
 |-  ( ph -> ( ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) " Z ) = ran ( k e. Z |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) )
42 38 40 41 3eqtr4d 
 |-  ( ph -> ( ( k e. RR |-> inf ( ( ( ( F |` Z ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) " Z ) = ( ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) " Z ) )
43 42 supeq1d 
 |-  ( ph -> sup ( ( ( k e. RR |-> inf ( ( ( ( F |` Z ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) " Z ) , RR* , < ) = sup ( ( ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) " Z ) , RR* , < ) )
44 eqid 
 |-  ( k e. RR |-> inf ( ( ( ( F |` Z ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( k e. RR |-> inf ( ( ( ( F |` Z ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
45 3 resexd 
 |-  ( ph -> ( F |` Z ) e. _V )
46 2 supeq1i 
 |-  sup ( Z , RR* , < ) = sup ( ( M [,) +oo ) , RR* , < )
47 46 a1i 
 |-  ( ph -> sup ( Z , RR* , < ) = sup ( ( M [,) +oo ) , RR* , < ) )
48 1 renepnfd 
 |-  ( ph -> M =/= +oo )
49 icopnfsup 
 |-  ( ( M e. RR* /\ M =/= +oo ) -> sup ( ( M [,) +oo ) , RR* , < ) = +oo )
50 4 48 49 syl2anc 
 |-  ( ph -> sup ( ( M [,) +oo ) , RR* , < ) = +oo )
51 47 50 eqtrd 
 |-  ( ph -> sup ( Z , RR* , < ) = +oo )
52 44 45 39 51 liminfval2 
 |-  ( ph -> ( liminf ` ( F |` Z ) ) = sup ( ( ( k e. RR |-> inf ( ( ( ( F |` Z ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) " Z ) , RR* , < ) )
53 eqid 
 |-  ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
54 53 3 39 51 liminfval2 
 |-  ( ph -> ( liminf ` F ) = sup ( ( ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) " Z ) , RR* , < ) )
55 43 52 54 3eqtr4d 
 |-  ( ph -> ( liminf ` ( F |` Z ) ) = ( liminf ` F ) )