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 φ F V
limsupresxr.2 φ Fun F
limsupresxr.3 A = F -1 *
Assertion limsupresxr φ lim sup F A = lim sup F

Proof

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