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