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 ) )