Metamath Proof Explorer


Theorem limsupresxr

Description: The superior limit of a function only depends on the restriction of that function to the preimage of the set of extended reals. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses limsupresxr.1
|- ( ph -> F e. V )
limsupresxr.2
|- ( ph -> Fun F )
limsupresxr.3
|- A = ( `' F " RR* )
Assertion limsupresxr
|- ( ph -> ( limsup ` ( F |` A ) ) = ( limsup ` F ) )

Proof

Step Hyp Ref Expression
1 limsupresxr.1
 |-  ( ph -> F e. V )
2 limsupresxr.2
 |-  ( ph -> Fun F )
3 limsupresxr.3
 |-  A = ( `' F " RR* )
4 resimass
 |-  ( ( F |` A ) " ( k [,) +oo ) ) C_ ( F " ( k [,) +oo ) )
5 4 a1i
 |-  ( ph -> ( ( F |` A ) " ( k [,) +oo ) ) C_ ( F " ( k [,) +oo ) ) )
6 5 ssrind
 |-  ( ph -> ( ( ( F |` A ) " ( k [,) +oo ) ) i^i RR* ) C_ ( ( F " ( k [,) +oo ) ) i^i RR* ) )
7 2 funfnd
 |-  ( ph -> F Fn dom F )
8 elinel1
 |-  ( y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) -> y e. ( F " ( k [,) +oo ) ) )
9 fvelima2
 |-  ( ( F Fn dom F /\ y e. ( F " ( k [,) +oo ) ) ) -> E. x e. ( dom F i^i ( k [,) +oo ) ) ( F ` x ) = y )
10 7 8 9 syl2an
 |-  ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) -> E. x e. ( dom F i^i ( k [,) +oo ) ) ( F ` x ) = y )
11 elinel1
 |-  ( x e. ( dom F i^i ( k [,) +oo ) ) -> x e. dom F )
12 11 3ad2ant2
 |-  ( ( y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) /\ x e. ( dom F i^i ( k [,) +oo ) ) /\ ( F ` x ) = y ) -> x e. dom F )
13 simpr
 |-  ( ( y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) /\ ( F ` x ) = y ) -> ( F ` x ) = y )
14 elinel2
 |-  ( y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) -> y e. RR* )
15 14 adantr
 |-  ( ( y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) /\ ( F ` x ) = y ) -> y e. RR* )
16 13 15 eqeltrd
 |-  ( ( y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) /\ ( F ` x ) = y ) -> ( F ` x ) e. RR* )
17 16 3adant2
 |-  ( ( y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) /\ x e. ( dom F i^i ( k [,) +oo ) ) /\ ( F ` x ) = y ) -> ( F ` x ) e. RR* )
18 12 17 jca
 |-  ( ( y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) /\ x e. ( dom F i^i ( k [,) +oo ) ) /\ ( F ` x ) = y ) -> ( x e. dom F /\ ( F ` x ) e. RR* ) )
19 18 3adant1l
 |-  ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) /\ ( F ` x ) = y ) -> ( x e. dom F /\ ( F ` x ) e. RR* ) )
20 simp1l
 |-  ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) /\ ( F ` x ) = y ) -> ph )
21 elpreima
 |-  ( F Fn dom F -> ( x e. ( `' F " RR* ) <-> ( x e. dom F /\ ( F ` x ) e. RR* ) ) )
22 7 21 syl
 |-  ( ph -> ( x e. ( `' F " RR* ) <-> ( x e. dom F /\ ( F ` x ) e. RR* ) ) )
23 20 22 syl
 |-  ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) /\ ( F ` x ) = y ) -> ( x e. ( `' F " RR* ) <-> ( x e. dom F /\ ( F ` x ) e. RR* ) ) )
24 19 23 mpbird
 |-  ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) /\ ( F ` x ) = y ) -> x e. ( `' F " RR* ) )
25 24 3 eleqtrrdi
 |-  ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) /\ ( F ` x ) = y ) -> x e. A )
26 25 3expa
 |-  ( ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) ) /\ ( F ` x ) = y ) -> x e. A )
27 26 fvresd
 |-  ( ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) ) /\ ( F ` x ) = y ) -> ( ( F |` A ) ` x ) = ( F ` x ) )
28 simpr
 |-  ( ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) ) /\ ( F ` x ) = y ) -> ( F ` x ) = y )
29 27 28 eqtr2d
 |-  ( ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) ) /\ ( F ` x ) = y ) -> y = ( ( F |` A ) ` x ) )
30 simplll
 |-  ( ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) ) /\ ( F ` x ) = y ) -> ph )
31 2 funresd
 |-  ( ph -> Fun ( F |` A ) )
32 30 31 syl
 |-  ( ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) ) /\ ( F ` x ) = y ) -> Fun ( F |` A ) )
33 11 ad2antlr
 |-  ( ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) ) /\ ( F ` x ) = y ) -> x e. dom F )
34 26 33 elind
 |-  ( ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) ) /\ ( F ` x ) = y ) -> x e. ( A i^i dom F ) )
35 dmres
 |-  dom ( F |` A ) = ( A i^i dom F )
36 34 35 eleqtrrdi
 |-  ( ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) ) /\ ( F ` x ) = y ) -> x e. dom ( F |` A ) )
37 32 36 jca
 |-  ( ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) ) /\ ( F ` x ) = y ) -> ( Fun ( F |` A ) /\ x e. dom ( F |` A ) ) )
38 elinel2
 |-  ( x e. ( dom F i^i ( k [,) +oo ) ) -> x e. ( k [,) +oo ) )
39 38 ad2antlr
 |-  ( ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) ) /\ ( F ` x ) = y ) -> x e. ( k [,) +oo ) )
40 funfvima
 |-  ( ( Fun ( F |` A ) /\ x e. dom ( F |` A ) ) -> ( x e. ( k [,) +oo ) -> ( ( F |` A ) ` x ) e. ( ( F |` A ) " ( k [,) +oo ) ) ) )
41 37 39 40 sylc
 |-  ( ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) ) /\ ( F ` x ) = y ) -> ( ( F |` A ) ` x ) e. ( ( F |` A ) " ( k [,) +oo ) ) )
42 29 41 eqeltrd
 |-  ( ( ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) /\ x e. ( dom F i^i ( k [,) +oo ) ) ) /\ ( F ` x ) = y ) -> y e. ( ( F |` A ) " ( k [,) +oo ) ) )
43 42 rexlimdva2
 |-  ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) -> ( E. x e. ( dom F i^i ( k [,) +oo ) ) ( F ` x ) = y -> y e. ( ( F |` A ) " ( k [,) +oo ) ) ) )
44 10 43 mpd
 |-  ( ( ph /\ y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) -> y e. ( ( F |` A ) " ( k [,) +oo ) ) )
45 44 ralrimiva
 |-  ( ph -> A. y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) y e. ( ( F |` A ) " ( k [,) +oo ) ) )
46 dfss3
 |-  ( ( ( F " ( k [,) +oo ) ) i^i RR* ) C_ ( ( F |` A ) " ( k [,) +oo ) ) <-> A. y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) y e. ( ( F |` A ) " ( k [,) +oo ) ) )
47 45 46 sylibr
 |-  ( ph -> ( ( F " ( k [,) +oo ) ) i^i RR* ) C_ ( ( F |` A ) " ( k [,) +oo ) ) )
48 inss2
 |-  ( ( F " ( k [,) +oo ) ) i^i RR* ) C_ RR*
49 48 a1i
 |-  ( ph -> ( ( F " ( k [,) +oo ) ) i^i RR* ) C_ RR* )
50 47 49 ssind
 |-  ( ph -> ( ( F " ( k [,) +oo ) ) i^i RR* ) C_ ( ( ( F |` A ) " ( k [,) +oo ) ) i^i RR* ) )
51 6 50 eqssd
 |-  ( ph -> ( ( ( F |` A ) " ( k [,) +oo ) ) i^i RR* ) = ( ( F " ( k [,) +oo ) ) i^i RR* ) )
52 51 supeq1d
 |-  ( ph -> sup ( ( ( ( F |` A ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) = sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
53 52 mpteq2dv
 |-  ( ph -> ( k e. RR |-> sup ( ( ( ( F |` A ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) )
54 53 rneqd
 |-  ( ph -> ran ( k e. RR |-> sup ( ( ( ( F |` A ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ran ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) )
55 54 infeq1d
 |-  ( ph -> inf ( ran ( k e. RR |-> sup ( ( ( ( F |` A ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) = inf ( ran ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
56 1 resexd
 |-  ( ph -> ( F |` A ) e. _V )
57 eqid
 |-  ( k e. RR |-> sup ( ( ( ( F |` A ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( k e. RR |-> sup ( ( ( ( F |` A ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
58 57 limsupval
 |-  ( ( F |` A ) e. _V -> ( limsup ` ( F |` A ) ) = inf ( ran ( k e. RR |-> sup ( ( ( ( F |` A ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
59 56 58 syl
 |-  ( ph -> ( limsup ` ( F |` A ) ) = inf ( ran ( k e. RR |-> sup ( ( ( ( F |` A ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
60 eqid
 |-  ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
61 60 limsupval
 |-  ( F e. V -> ( limsup ` F ) = inf ( ran ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
62 1 61 syl
 |-  ( ph -> ( limsup ` F ) = inf ( ran ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
63 55 59 62 3eqtr4d
 |-  ( ph -> ( limsup ` ( F |` A ) ) = ( limsup ` F ) )