This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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