Metamath Proof Explorer


Theorem liminfresxr

Description: The inferior limit of a function only depends on the preimage of the extended real part. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses liminfresxr.1 ( 𝜑𝐹𝑉 )
liminfresxr.2 ( 𝜑 → Fun 𝐹 )
liminfresxr.3 𝐴 = ( 𝐹 “ ℝ* )
Assertion liminfresxr ( 𝜑 → ( lim inf ‘ ( 𝐹𝐴 ) ) = ( lim inf ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 liminfresxr.1 ( 𝜑𝐹𝑉 )
2 liminfresxr.2 ( 𝜑 → Fun 𝐹 )
3 liminfresxr.3 𝐴 = ( 𝐹 “ ℝ* )
4 resimass ( ( 𝐹𝐴 ) “ ( 𝑘 [,) +∞ ) ) ⊆ ( 𝐹 “ ( 𝑘 [,) +∞ ) )
5 4 a1i ( 𝜑 → ( ( 𝐹𝐴 ) “ ( 𝑘 [,) +∞ ) ) ⊆ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
6 5 ssrind ( 𝜑 → ( ( ( 𝐹𝐴 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) )
7 2 funfnd ( 𝜑𝐹 Fn dom 𝐹 )
8 elinel1 ( 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) → 𝑦 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
9 fvelima2 ( ( 𝐹 Fn dom 𝐹𝑦 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ) → ∃ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ( 𝐹𝑥 ) = 𝑦 )
10 7 8 9 syl2an ( ( 𝜑𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) → ∃ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ( 𝐹𝑥 ) = 𝑦 )
11 elinel1 ( 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) → 𝑥 ∈ dom 𝐹 )
12 11 3ad2ant2 ( ( 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ∧ ( 𝐹𝑥 ) = 𝑦 ) → 𝑥 ∈ dom 𝐹 )
13 simpr ( ( 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ∧ ( 𝐹𝑥 ) = 𝑦 ) → ( 𝐹𝑥 ) = 𝑦 )
14 elinel2 ( 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) → 𝑦 ∈ ℝ* )
15 14 adantr ( ( 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ∧ ( 𝐹𝑥 ) = 𝑦 ) → 𝑦 ∈ ℝ* )
16 13 15 eqeltrd ( ( 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ∧ ( 𝐹𝑥 ) = 𝑦 ) → ( 𝐹𝑥 ) ∈ ℝ* )
17 16 3adant2 ( ( 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ∧ ( 𝐹𝑥 ) = 𝑦 ) → ( 𝐹𝑥 ) ∈ ℝ* )
18 12 17 jca ( ( 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ∧ ( 𝐹𝑥 ) = 𝑦 ) → ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹𝑥 ) ∈ ℝ* ) )
19 18 3adant1l ( ( ( 𝜑𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ∧ ( 𝐹𝑥 ) = 𝑦 ) → ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹𝑥 ) ∈ ℝ* ) )
20 simp1l ( ( ( 𝜑𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ∧ ( 𝐹𝑥 ) = 𝑦 ) → 𝜑 )
21 elpreima ( 𝐹 Fn dom 𝐹 → ( 𝑥 ∈ ( 𝐹 “ ℝ* ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹𝑥 ) ∈ ℝ* ) ) )
22 7 21 syl ( 𝜑 → ( 𝑥 ∈ ( 𝐹 “ ℝ* ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹𝑥 ) ∈ ℝ* ) ) )
23 20 22 syl ( ( ( 𝜑𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ∧ ( 𝐹𝑥 ) = 𝑦 ) → ( 𝑥 ∈ ( 𝐹 “ ℝ* ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹𝑥 ) ∈ ℝ* ) ) )
24 19 23 mpbird ( ( ( 𝜑𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ∧ ( 𝐹𝑥 ) = 𝑦 ) → 𝑥 ∈ ( 𝐹 “ ℝ* ) )
25 24 3 eleqtrrdi ( ( ( 𝜑𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ∧ ( 𝐹𝑥 ) = 𝑦 ) → 𝑥𝐴 )
26 25 3expa ( ( ( ( 𝜑𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ ( 𝐹𝑥 ) = 𝑦 ) → 𝑥𝐴 )
27 26 fvresd ( ( ( ( 𝜑𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ ( 𝐹𝑥 ) = 𝑦 ) → ( ( 𝐹𝐴 ) ‘ 𝑥 ) = ( 𝐹𝑥 ) )
28 simpr ( ( ( ( 𝜑𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ ( 𝐹𝑥 ) = 𝑦 ) → ( 𝐹𝑥 ) = 𝑦 )
29 27 28 eqtr2d ( ( ( ( 𝜑𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ ( 𝐹𝑥 ) = 𝑦 ) → 𝑦 = ( ( 𝐹𝐴 ) ‘ 𝑥 ) )
30 simplll ( ( ( ( 𝜑𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ ( 𝐹𝑥 ) = 𝑦 ) → 𝜑 )
31 2 funresd ( 𝜑 → Fun ( 𝐹𝐴 ) )
32 30 31 syl ( ( ( ( 𝜑𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ ( 𝐹𝑥 ) = 𝑦 ) → Fun ( 𝐹𝐴 ) )
33 11 ad2antlr ( ( ( ( 𝜑𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ ( 𝐹𝑥 ) = 𝑦 ) → 𝑥 ∈ dom 𝐹 )
34 26 33 elind ( ( ( ( 𝜑𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ ( 𝐹𝑥 ) = 𝑦 ) → 𝑥 ∈ ( 𝐴 ∩ dom 𝐹 ) )
35 dmres dom ( 𝐹𝐴 ) = ( 𝐴 ∩ dom 𝐹 )
36 34 35 eleqtrrdi ( ( ( ( 𝜑𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ ( 𝐹𝑥 ) = 𝑦 ) → 𝑥 ∈ dom ( 𝐹𝐴 ) )
37 32 36 jca ( ( ( ( 𝜑𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ ( 𝐹𝑥 ) = 𝑦 ) → ( Fun ( 𝐹𝐴 ) ∧ 𝑥 ∈ dom ( 𝐹𝐴 ) ) )
38 elinel2 ( 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) → 𝑥 ∈ ( 𝑘 [,) +∞ ) )
39 38 ad2antlr ( ( ( ( 𝜑𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ ( 𝐹𝑥 ) = 𝑦 ) → 𝑥 ∈ ( 𝑘 [,) +∞ ) )
40 funfvima ( ( Fun ( 𝐹𝐴 ) ∧ 𝑥 ∈ dom ( 𝐹𝐴 ) ) → ( 𝑥 ∈ ( 𝑘 [,) +∞ ) → ( ( 𝐹𝐴 ) ‘ 𝑥 ) ∈ ( ( 𝐹𝐴 ) “ ( 𝑘 [,) +∞ ) ) ) )
41 37 39 40 sylc ( ( ( ( 𝜑𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ ( 𝐹𝑥 ) = 𝑦 ) → ( ( 𝐹𝐴 ) ‘ 𝑥 ) ∈ ( ( 𝐹𝐴 ) “ ( 𝑘 [,) +∞ ) ) )
42 29 41 eqeltrd ( ( ( ( 𝜑𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ ( 𝐹𝑥 ) = 𝑦 ) → 𝑦 ∈ ( ( 𝐹𝐴 ) “ ( 𝑘 [,) +∞ ) ) )
43 42 rexlimdva2 ( ( 𝜑𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) → ( ∃ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ( 𝐹𝑥 ) = 𝑦𝑦 ∈ ( ( 𝐹𝐴 ) “ ( 𝑘 [,) +∞ ) ) ) )
44 10 43 mpd ( ( 𝜑𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) → 𝑦 ∈ ( ( 𝐹𝐴 ) “ ( 𝑘 [,) +∞ ) ) )
45 44 ralrimiva ( 𝜑 → ∀ 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) 𝑦 ∈ ( ( 𝐹𝐴 ) “ ( 𝑘 [,) +∞ ) ) )
46 dfss3 ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ( ( 𝐹𝐴 ) “ ( 𝑘 [,) +∞ ) ) ↔ ∀ 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) 𝑦 ∈ ( ( 𝐹𝐴 ) “ ( 𝑘 [,) +∞ ) ) )
47 45 46 sylibr ( 𝜑 → ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ( ( 𝐹𝐴 ) “ ( 𝑘 [,) +∞ ) ) )
48 inss2 ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ*
49 48 a1i ( 𝜑 → ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ* )
50 47 49 ssind ( 𝜑 → ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ( ( ( 𝐹𝐴 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) )
51 6 50 eqssd ( 𝜑 → ( ( ( 𝐹𝐴 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) = ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) )
52 51 infeq1d ( 𝜑 → inf ( ( ( ( 𝐹𝐴 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) = inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
53 52 mpteq2dv ( 𝜑 → ( 𝑘 ∈ ℝ ↦ inf ( ( ( ( 𝐹𝐴 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) )
54 53 rneqd ( 𝜑 → ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( ( 𝐹𝐴 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) )
55 54 supeq1d ( 𝜑 → sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( ( 𝐹𝐴 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) = sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
56 1 resexd ( 𝜑 → ( 𝐹𝐴 ) ∈ V )
57 eqid ( 𝑘 ∈ ℝ ↦ inf ( ( ( ( 𝐹𝐴 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑘 ∈ ℝ ↦ inf ( ( ( ( 𝐹𝐴 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
58 57 liminfval ( ( 𝐹𝐴 ) ∈ V → ( lim inf ‘ ( 𝐹𝐴 ) ) = sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( ( 𝐹𝐴 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
59 56 58 syl ( 𝜑 → ( lim inf ‘ ( 𝐹𝐴 ) ) = sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( ( 𝐹𝐴 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
60 eqid ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
61 60 liminfval ( 𝐹𝑉 → ( lim inf ‘ 𝐹 ) = sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
62 1 61 syl ( 𝜑 → ( lim inf ‘ 𝐹 ) = sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
63 55 59 62 3eqtr4d ( 𝜑 → ( lim inf ‘ ( 𝐹𝐴 ) ) = ( lim inf ‘ 𝐹 ) )