Metamath Proof Explorer

Theorem liminfvalxr

Description: Alternate definition of liminf when F is an extended real-valued function. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses liminfvalxr.1 ⊢ Ⅎ 𝑥 𝐹
liminfvalxr.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
liminfvalxr.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
Assertion liminfvalxr ( 𝜑 → ( lim inf ‘ 𝐹 ) = -𝑒 ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 liminfvalxr.1 ⊢ Ⅎ 𝑥 𝐹
2 liminfvalxr.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3 liminfvalxr.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
4 nftru ⊢ Ⅎ 𝑘 ⊤
5 inss2 ⊢ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ*
6 infxrcl ⊢ ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ* → inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ* )
7 5 6 ax-mp ⊢ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ*
8 7 a1i ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℝ ) → inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ* )
9 4 8 supminfxrrnmpt ⊢ ( ⊤ → sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) = -𝑒 inf ( ran ( 𝑘 ∈ ℝ ↦ -𝑒 inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
10 9 mptru ⊢ sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) = -𝑒 inf ( ran ( 𝑘 ∈ ℝ ↦ -𝑒 inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < )
11 10 a1i ⊢ ( 𝜑 → sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) = -𝑒 inf ( ran ( 𝑘 ∈ ℝ ↦ -𝑒 inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
12 tru ⊢ ⊤
13 inss2 ⊢ ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ*
14 13 a1i ⊢ ( ⊤ → ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ* )
15 14 supminfxr2 ⊢ ( ⊤ → sup ( ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) = -𝑒 inf ( { 𝑧 ∈ ℝ* ∣ -𝑒 𝑧 ∈ ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) } , ℝ* , < ) )
16 12 15 ax-mp ⊢ sup ( ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) = -𝑒 inf ( { 𝑧 ∈ ℝ* ∣ -𝑒 𝑧 ∈ ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) } , ℝ* , < )
17 16 a1i ⊢ ( 𝜑 → sup ( ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) = -𝑒 inf ( { 𝑧 ∈ ℝ* ∣ -𝑒 𝑧 ∈ ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) } , ℝ* , < ) )
18 elinel1 ⊢ ( -𝑒 𝑧 ∈ ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) → -𝑒 𝑧 ∈ ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) )
19 nfmpt1 ⊢ Ⅎ 𝑦 ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) )
20 xnegex ⊢ -𝑒 ( 𝐹 ‘ 𝑦 ) ∈ V
21 eqid ⊢ ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) = ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) )
22 20 21 fnmpti ⊢ ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) Fn 𝐴
23 22 a1i ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) Fn 𝐴 )
24 23 adantr ⊢ ( ( 𝜑 ∧ -𝑒 𝑧 ∈ ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ) → ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) Fn 𝐴 )
25 simpr ⊢ ( ( 𝜑 ∧ -𝑒 𝑧 ∈ ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ) → -𝑒 𝑧 ∈ ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) )
26 19 24 25 fvelimad ⊢ ( ( 𝜑 ∧ -𝑒 𝑧 ∈ ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ) → ∃ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ‘ 𝑦 ) = -𝑒 𝑧 )
27 26 3adant2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ∧ -𝑒 𝑧 ∈ ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ) → ∃ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ‘ 𝑦 ) = -𝑒 𝑧 )
28 18 27 syl3an3 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ∧ -𝑒 𝑧 ∈ ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) → ∃ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ‘ 𝑦 ) = -𝑒 𝑧 )
29 elinel2 ⊢ ( -𝑒 𝑧 ∈ ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) → -𝑒 𝑧 ∈ ℝ* )
30 elinel1 ⊢ ( 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) → 𝑦 ∈ 𝐴 )
31 20 a1i ⊢ ( 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) → -𝑒 ( 𝐹 ‘ 𝑦 ) ∈ V )
32 21 fvmpt2 ⊢ ( ( 𝑦 ∈ 𝐴 ∧ -𝑒 ( 𝐹 ‘ 𝑦 ) ∈ V ) → ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ‘ 𝑦 ) = -𝑒 ( 𝐹 ‘ 𝑦 ) )
33 30 31 32 syl2anc ⊢ ( 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) → ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ‘ 𝑦 ) = -𝑒 ( 𝐹 ‘ 𝑦 ) )
34 33 eqcomd ⊢ ( 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) → -𝑒 ( 𝐹 ‘ 𝑦 ) = ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ‘ 𝑦 ) )
35 34 adantr ⊢ ( ( 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ‘ 𝑦 ) = -𝑒 𝑧 ) → -𝑒 ( 𝐹 ‘ 𝑦 ) = ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ‘ 𝑦 ) )
36 simpr ⊢ ( ( 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ‘ 𝑦 ) = -𝑒 𝑧 ) → ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ‘ 𝑦 ) = -𝑒 𝑧 )
37 35 36 eqtrd ⊢ ( ( 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ‘ 𝑦 ) = -𝑒 𝑧 ) → -𝑒 ( 𝐹 ‘ 𝑦 ) = -𝑒 𝑧 )
38 37 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ‘ 𝑦 ) = -𝑒 𝑧 ) → -𝑒 ( 𝐹 ‘ 𝑦 ) = -𝑒 𝑧 )
39 eqcom ⊢ ( -𝑒 ( 𝐹 ‘ 𝑦 ) = -𝑒 𝑧 ↔ -𝑒 𝑧 = -𝑒 ( 𝐹 ‘ 𝑦 ) )
40 39 bilani ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ -𝑒 ( 𝐹 ‘ 𝑦 ) = -𝑒 𝑧 ) → -𝑒 𝑧 = -𝑒 ( 𝐹 ‘ 𝑦 ) )
41 simplr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → 𝑧 ∈ ℝ* )
42 3 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → 𝐹 : 𝐴 ⟶ ℝ* )
43 30 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → 𝑦 ∈ 𝐴 )
44 42 43 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ* )
45 44 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ* )
46 xneg11 ⊢ ( ( 𝑧 ∈ ℝ* ∧ ( 𝐹 ‘ 𝑦 ) ∈ ℝ* ) → ( -𝑒 𝑧 = -𝑒 ( 𝐹 ‘ 𝑦 ) ↔ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) )
47 41 45 46 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → ( -𝑒 𝑧 = -𝑒 ( 𝐹 ‘ 𝑦 ) ↔ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) )
48 47 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ -𝑒 ( 𝐹 ‘ 𝑦 ) = -𝑒 𝑧 ) → ( -𝑒 𝑧 = -𝑒 ( 𝐹 ‘ 𝑦 ) ↔ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) )
49 40 48 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ -𝑒 ( 𝐹 ‘ 𝑦 ) = -𝑒 𝑧 ) → 𝑧 = ( 𝐹 ‘ 𝑦 ) )
50 3 ffund ⊢ ( 𝜑 → Fun 𝐹 )
51 50 30 anim12i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → ( Fun 𝐹 ∧ 𝑦 ∈ 𝐴 ) )
52 51 simpld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → Fun 𝐹 )
53 3 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
54 53 eqcomd ⊢ ( 𝜑 → 𝐴 = dom 𝐹 )
55 54 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → 𝐴 = dom 𝐹 )
56 43 55 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → 𝑦 ∈ dom 𝐹 )
57 52 56 jca ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → ( Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) )
58 elinel2 ⊢ ( 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) → 𝑦 ∈ ( 𝑘 [,) +∞ ) )
59 58 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → 𝑦 ∈ ( 𝑘 [,) +∞ ) )
60 funfvima ⊢ ( ( Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) → ( 𝑦 ∈ ( 𝑘 [,) +∞ ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ) )
61 57 59 60 sylc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
62 61 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ -𝑒 ( 𝐹 ‘ 𝑦 ) = -𝑒 𝑧 ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
63 49 62 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ -𝑒 ( 𝐹 ‘ 𝑦 ) = -𝑒 𝑧 ) → 𝑧 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
64 38 63 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ‘ 𝑦 ) = -𝑒 𝑧 ) → 𝑧 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
65 64 rexlimdva2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) → ( ∃ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ‘ 𝑦 ) = -𝑒 𝑧 → 𝑧 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ) )
66 65 3adant3 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ∧ -𝑒 𝑧 ∈ ℝ* ) → ( ∃ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ‘ 𝑦 ) = -𝑒 𝑧 → 𝑧 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ) )
67 29 66 syl3an3 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ∧ -𝑒 𝑧 ∈ ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) → ( ∃ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ‘ 𝑦 ) = -𝑒 𝑧 → 𝑧 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ) )
68 28 67 mpd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ∧ -𝑒 𝑧 ∈ ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) → 𝑧 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
69 68 rabssdv ⊢ ( 𝜑 → { 𝑧 ∈ ℝ* ∣ -𝑒 𝑧 ∈ ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) } ⊆ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
70 ssrab2 ⊢ { 𝑧 ∈ ℝ* ∣ -𝑒 𝑧 ∈ ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) } ⊆ ℝ*
71 70 a1i ⊢ ( 𝜑 → { 𝑧 ∈ ℝ* ∣ -𝑒 𝑧 ∈ ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) } ⊆ ℝ* )
72 69 71 ssind ⊢ ( 𝜑 → { 𝑧 ∈ ℝ* ∣ -𝑒 𝑧 ∈ ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) } ⊆ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) )
73 5 a1i ⊢ ( 𝜑 → ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ* )
74 3 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
75 74 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) → 𝐹 Fn 𝐴 )
76 elinel1 ⊢ ( 𝑧 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) → 𝑧 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
77 76 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) → 𝑧 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
78 fvelima2 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑧 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ) → ∃ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) = 𝑧 )
79 75 77 78 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) → ∃ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) = 𝑧 )
80 elinel2 ⊢ ( 𝑧 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) → 𝑧 ∈ ℝ* )
81 eqcom ⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑧 ↔ 𝑧 = ( 𝐹 ‘ 𝑦 ) )
82 81 bilani ⊢ ( ( 𝑧 ∈ ℝ* ∧ ( 𝐹 ‘ 𝑦 ) = 𝑧 ) → 𝑧 = ( 𝐹 ‘ 𝑦 ) )
83 82 xnegeqd ⊢ ( ( 𝑧 ∈ ℝ* ∧ ( 𝐹 ‘ 𝑦 ) = 𝑧 ) → -𝑒 𝑧 = -𝑒 ( 𝐹 ‘ 𝑦 ) )
84 83 ex ⊢ ( 𝑧 ∈ ℝ* → ( ( 𝐹 ‘ 𝑦 ) = 𝑧 → -𝑒 𝑧 = -𝑒 ( 𝐹 ‘ 𝑦 ) ) )
85 84 reximdv ⊢ ( 𝑧 ∈ ℝ* → ( ∃ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) = 𝑧 → ∃ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) -𝑒 𝑧 = -𝑒 ( 𝐹 ‘ 𝑦 ) ) )
86 80 85 syl ⊢ ( 𝑧 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) → ( ∃ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) = 𝑧 → ∃ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) -𝑒 𝑧 = -𝑒 ( 𝐹 ‘ 𝑦 ) ) )
87 86 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) → ( ∃ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) = 𝑧 → ∃ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) -𝑒 𝑧 = -𝑒 ( 𝐹 ‘ 𝑦 ) ) )
88 79 87 mpd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) → ∃ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) -𝑒 𝑧 = -𝑒 ( 𝐹 ‘ 𝑦 ) )
89 xnegex ⊢ -𝑒 𝑧 ∈ V
90 elmptima ⊢ ( -𝑒 𝑧 ∈ V → ( -𝑒 𝑧 ∈ ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ↔ ∃ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) -𝑒 𝑧 = -𝑒 ( 𝐹 ‘ 𝑦 ) ) )
91 89 90 ax-mp ⊢ ( -𝑒 𝑧 ∈ ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ↔ ∃ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) -𝑒 𝑧 = -𝑒 ( 𝐹 ‘ 𝑦 ) )
92 88 91 sylibr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) → -𝑒 𝑧 ∈ ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) )
93 73 sselda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) → 𝑧 ∈ ℝ* )
94 93 xnegcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) → -𝑒 𝑧 ∈ ℝ* )
95 92 94 elind ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) → -𝑒 𝑧 ∈ ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) )
96 73 95 ssrabdv ⊢ ( 𝜑 → ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ { 𝑧 ∈ ℝ* ∣ -𝑒 𝑧 ∈ ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) } )
97 72 96 eqssd ⊢ ( 𝜑 → { 𝑧 ∈ ℝ* ∣ -𝑒 𝑧 ∈ ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) } = ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) )
98 97 infeq1d ⊢ ( 𝜑 → inf ( { 𝑧 ∈ ℝ* ∣ -𝑒 𝑧 ∈ ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) } , ℝ* , < ) = inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
99 98 xnegeqd ⊢ ( 𝜑 → -𝑒 inf ( { 𝑧 ∈ ℝ* ∣ -𝑒 𝑧 ∈ ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) } , ℝ* , < ) = -𝑒 inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
100 17 99 eqtr2d ⊢ ( 𝜑 → -𝑒 inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) = sup ( ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
101 100 mpteq2dv ⊢ ( 𝜑 → ( 𝑘 ∈ ℝ ↦ -𝑒 inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) )
102 101 rneqd ⊢ ( 𝜑 → ran ( 𝑘 ∈ ℝ ↦ -𝑒 inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) )
103 102 infeq1d ⊢ ( 𝜑 → inf ( ran ( 𝑘 ∈ ℝ ↦ -𝑒 inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) = inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
104 103 xnegeqd ⊢ ( 𝜑 → -𝑒 inf ( ran ( 𝑘 ∈ ℝ ↦ -𝑒 inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) = -𝑒 inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
105 11 104 eqtrd ⊢ ( 𝜑 → sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) = -𝑒 inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
106 3 2 fexd ⊢ ( 𝜑 → 𝐹 ∈ V )
107 eqid ⊢ ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
108 107 liminfval ⊢ ( 𝐹 ∈ V → ( lim inf ‘ 𝐹 ) = sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
109 106 108 syl ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
110 2 mptexd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ∈ V )
111 eqid ⊢ ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
112 111 limsupval ⊢ ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ∈ V → ( lim sup ‘ ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ) = inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
113 110 112 syl ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ) = inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
114 113 xnegeqd ⊢ ( 𝜑 → -𝑒 ( lim sup ‘ ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ) = -𝑒 inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
115 105 109 114 3eqtr4d ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = -𝑒 ( lim sup ‘ ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ) )
116 nfcv ⊢ Ⅎ 𝑥 𝑦
117 1 116 nffv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑦 )
118 117 nfxneg ⊢ Ⅎ 𝑥 -𝑒 ( 𝐹 ‘ 𝑦 )
119 nfcv ⊢ Ⅎ 𝑦 -𝑒 ( 𝐹 ‘ 𝑥 )
120 fveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
121 120 xnegeqd ⊢ ( 𝑦 = 𝑥 → -𝑒 ( 𝐹 ‘ 𝑦 ) = -𝑒 ( 𝐹 ‘ 𝑥 ) )
122 118 119 121 cbvmpt ⊢ ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) = ( 𝑥 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑥 ) )
123 122 fveq2i ⊢ ( lim sup ‘ ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ) = ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑥 ) ) )
124 123 xnegeqi ⊢ -𝑒 ( lim sup ‘ ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ) = -𝑒 ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑥 ) ) )
125 124 a1i ⊢ ( 𝜑 → -𝑒 ( lim sup ‘ ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ) = -𝑒 ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑥 ) ) ) )
126 115 125 eqtrd ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = -𝑒 ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑥 ) ) ) )