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 biimpi ⊢ ( -𝑒 ( 𝐹 ‘ 𝑦 ) = -𝑒 𝑧 → -𝑒 𝑧 = -𝑒 ( 𝐹 ‘ 𝑦 ) )
41 40 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ -𝑒 ( 𝐹 ‘ 𝑦 ) = -𝑒 𝑧 ) → -𝑒 𝑧 = -𝑒 ( 𝐹 ‘ 𝑦 ) )
42 simplr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → 𝑧 ∈ ℝ* )
43 3 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → 𝐹 : 𝐴 ⟶ ℝ* )
44 30 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → 𝑦 ∈ 𝐴 )
45 43 44 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ* )
46 45 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ* )
47 xneg11 ⊢ ( ( 𝑧 ∈ ℝ* ∧ ( 𝐹 ‘ 𝑦 ) ∈ ℝ* ) → ( -𝑒 𝑧 = -𝑒 ( 𝐹 ‘ 𝑦 ) ↔ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) )
48 42 46 47 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → ( -𝑒 𝑧 = -𝑒 ( 𝐹 ‘ 𝑦 ) ↔ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) )
49 48 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ -𝑒 ( 𝐹 ‘ 𝑦 ) = -𝑒 𝑧 ) → ( -𝑒 𝑧 = -𝑒 ( 𝐹 ‘ 𝑦 ) ↔ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) )
50 41 49 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ -𝑒 ( 𝐹 ‘ 𝑦 ) = -𝑒 𝑧 ) → 𝑧 = ( 𝐹 ‘ 𝑦 ) )
51 3 ffund ⊢ ( 𝜑 → Fun 𝐹 )
52 51 30 anim12i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → ( Fun 𝐹 ∧ 𝑦 ∈ 𝐴 ) )
53 52 simpld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → Fun 𝐹 )
54 3 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
55 54 eqcomd ⊢ ( 𝜑 → 𝐴 = dom 𝐹 )
56 55 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → 𝐴 = dom 𝐹 )
57 44 56 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → 𝑦 ∈ dom 𝐹 )
58 53 57 jca ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → ( Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) )
59 elinel2 ⊢ ( 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) → 𝑦 ∈ ( 𝑘 [,) +∞ ) )
60 59 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → 𝑦 ∈ ( 𝑘 [,) +∞ ) )
61 funfvima ⊢ ( ( Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) → ( 𝑦 ∈ ( 𝑘 [,) +∞ ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ) )
62 58 60 61 sylc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
63 62 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ -𝑒 ( 𝐹 ‘ 𝑦 ) = -𝑒 𝑧 ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
64 50 63 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ -𝑒 ( 𝐹 ‘ 𝑦 ) = -𝑒 𝑧 ) → 𝑧 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
65 38 64 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ‘ 𝑦 ) = -𝑒 𝑧 ) → 𝑧 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
66 65 rexlimdva2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) → ( ∃ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ‘ 𝑦 ) = -𝑒 𝑧 → 𝑧 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ) )
67 66 3adant3 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ∧ -𝑒 𝑧 ∈ ℝ* ) → ( ∃ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ‘ 𝑦 ) = -𝑒 𝑧 → 𝑧 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ) )
68 29 67 syl3an3 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ∧ -𝑒 𝑧 ∈ ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) → ( ∃ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ‘ 𝑦 ) = -𝑒 𝑧 → 𝑧 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ) )
69 28 68 mpd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ∧ -𝑒 𝑧 ∈ ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) → 𝑧 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
70 69 rabssdv ⊢ ( 𝜑 → { 𝑧 ∈ ℝ* ∣ -𝑒 𝑧 ∈ ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) } ⊆ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
71 ssrab2 ⊢ { 𝑧 ∈ ℝ* ∣ -𝑒 𝑧 ∈ ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) } ⊆ ℝ*
72 71 a1i ⊢ ( 𝜑 → { 𝑧 ∈ ℝ* ∣ -𝑒 𝑧 ∈ ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) } ⊆ ℝ* )
73 70 72 ssind ⊢ ( 𝜑 → { 𝑧 ∈ ℝ* ∣ -𝑒 𝑧 ∈ ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) } ⊆ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) )
74 5 a1i ⊢ ( 𝜑 → ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ* )
75 3 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
76 75 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) → 𝐹 Fn 𝐴 )
77 elinel1 ⊢ ( 𝑧 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) → 𝑧 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
78 77 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) → 𝑧 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
79 fvelima2 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑧 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ) → ∃ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) = 𝑧 )
80 76 78 79 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) → ∃ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) = 𝑧 )
81 elinel2 ⊢ ( 𝑧 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) → 𝑧 ∈ ℝ* )
82 eqcom ⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑧 ↔ 𝑧 = ( 𝐹 ‘ 𝑦 ) )
83 82 biimpi ⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑧 → 𝑧 = ( 𝐹 ‘ 𝑦 ) )
84 83 adantl ⊢ ( ( 𝑧 ∈ ℝ* ∧ ( 𝐹 ‘ 𝑦 ) = 𝑧 ) → 𝑧 = ( 𝐹 ‘ 𝑦 ) )
85 84 xnegeqd ⊢ ( ( 𝑧 ∈ ℝ* ∧ ( 𝐹 ‘ 𝑦 ) = 𝑧 ) → -𝑒 𝑧 = -𝑒 ( 𝐹 ‘ 𝑦 ) )
86 simpl ⊢ ( ( 𝑧 ∈ ℝ* ∧ ( 𝐹 ‘ 𝑦 ) = 𝑧 ) → 𝑧 ∈ ℝ* )
87 84 86 eqeltrrd ⊢ ( ( 𝑧 ∈ ℝ* ∧ ( 𝐹 ‘ 𝑦 ) = 𝑧 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ* )
88 86 87 47 syl2anc ⊢ ( ( 𝑧 ∈ ℝ* ∧ ( 𝐹 ‘ 𝑦 ) = 𝑧 ) → ( -𝑒 𝑧 = -𝑒 ( 𝐹 ‘ 𝑦 ) ↔ 𝑧 = ( 𝐹 ‘ 𝑦 ) ) )
89 85 88 mpbid ⊢ ( ( 𝑧 ∈ ℝ* ∧ ( 𝐹 ‘ 𝑦 ) = 𝑧 ) → 𝑧 = ( 𝐹 ‘ 𝑦 ) )
90 89 xnegeqd ⊢ ( ( 𝑧 ∈ ℝ* ∧ ( 𝐹 ‘ 𝑦 ) = 𝑧 ) → -𝑒 𝑧 = -𝑒 ( 𝐹 ‘ 𝑦 ) )
91 90 ex ⊢ ( 𝑧 ∈ ℝ* → ( ( 𝐹 ‘ 𝑦 ) = 𝑧 → -𝑒 𝑧 = -𝑒 ( 𝐹 ‘ 𝑦 ) ) )
92 91 reximdv ⊢ ( 𝑧 ∈ ℝ* → ( ∃ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) = 𝑧 → ∃ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) -𝑒 𝑧 = -𝑒 ( 𝐹 ‘ 𝑦 ) ) )
93 81 92 syl ⊢ ( 𝑧 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) → ( ∃ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) = 𝑧 → ∃ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) -𝑒 𝑧 = -𝑒 ( 𝐹 ‘ 𝑦 ) ) )
94 93 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) → ( ∃ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) = 𝑧 → ∃ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) -𝑒 𝑧 = -𝑒 ( 𝐹 ‘ 𝑦 ) ) )
95 80 94 mpd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) → ∃ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) -𝑒 𝑧 = -𝑒 ( 𝐹 ‘ 𝑦 ) )
96 xnegex ⊢ -𝑒 𝑧 ∈ V
97 elmptima ⊢ ( -𝑒 𝑧 ∈ V → ( -𝑒 𝑧 ∈ ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ↔ ∃ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) -𝑒 𝑧 = -𝑒 ( 𝐹 ‘ 𝑦 ) ) )
98 96 97 ax-mp ⊢ ( -𝑒 𝑧 ∈ ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ↔ ∃ 𝑦 ∈ ( 𝐴 ∩ ( 𝑘 [,) +∞ ) ) -𝑒 𝑧 = -𝑒 ( 𝐹 ‘ 𝑦 ) )
99 95 98 sylibr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) → -𝑒 𝑧 ∈ ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) )
100 74 sselda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) → 𝑧 ∈ ℝ* )
101 100 xnegcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) → -𝑒 𝑧 ∈ ℝ* )
102 99 101 elind ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) → -𝑒 𝑧 ∈ ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) )
103 74 102 ssrabdv ⊢ ( 𝜑 → ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ { 𝑧 ∈ ℝ* ∣ -𝑒 𝑧 ∈ ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) } )
104 73 103 eqssd ⊢ ( 𝜑 → { 𝑧 ∈ ℝ* ∣ -𝑒 𝑧 ∈ ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) } = ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) )
105 104 infeq1d ⊢ ( 𝜑 → inf ( { 𝑧 ∈ ℝ* ∣ -𝑒 𝑧 ∈ ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) } , ℝ* , < ) = inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
106 105 xnegeqd ⊢ ( 𝜑 → -𝑒 inf ( { 𝑧 ∈ ℝ* ∣ -𝑒 𝑧 ∈ ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) } , ℝ* , < ) = -𝑒 inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
107 17 106 eqtr2d ⊢ ( 𝜑 → -𝑒 inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) = sup ( ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
108 107 mpteq2dv ⊢ ( 𝜑 → ( 𝑘 ∈ ℝ ↦ -𝑒 inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) )
109 108 rneqd ⊢ ( 𝜑 → ran ( 𝑘 ∈ ℝ ↦ -𝑒 inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) )
110 109 infeq1d ⊢ ( 𝜑 → inf ( ran ( 𝑘 ∈ ℝ ↦ -𝑒 inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) = inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
111 110 xnegeqd ⊢ ( 𝜑 → -𝑒 inf ( ran ( 𝑘 ∈ ℝ ↦ -𝑒 inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) = -𝑒 inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
112 11 111 eqtrd ⊢ ( 𝜑 → sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) = -𝑒 inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
113 3 2 fexd ⊢ ( 𝜑 → 𝐹 ∈ V )
114 eqid ⊢ ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
115 114 liminfval ⊢ ( 𝐹 ∈ V → ( lim inf ‘ 𝐹 ) = sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
116 113 115 syl ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
117 2 mptexd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ∈ V )
118 eqid ⊢ ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
119 118 limsupval ⊢ ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ∈ V → ( lim sup ‘ ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ) = inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
120 117 119 syl ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ) = inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
121 120 xnegeqd ⊢ ( 𝜑 → -𝑒 ( lim sup ‘ ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ) = -𝑒 inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
122 112 116 121 3eqtr4d ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = -𝑒 ( lim sup ‘ ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ) )
123 nfcv ⊢ Ⅎ 𝑥 𝑦
124 1 123 nffv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑦 )
125 124 nfxneg ⊢ Ⅎ 𝑥 -𝑒 ( 𝐹 ‘ 𝑦 )
126 nfcv ⊢ Ⅎ 𝑦 -𝑒 ( 𝐹 ‘ 𝑥 )
127 fveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
128 127 xnegeqd ⊢ ( 𝑦 = 𝑥 → -𝑒 ( 𝐹 ‘ 𝑦 ) = -𝑒 ( 𝐹 ‘ 𝑥 ) )
129 125 126 128 cbvmpt ⊢ ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) = ( 𝑥 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑥 ) )
130 129 fveq2i ⊢ ( lim sup ‘ ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ) = ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑥 ) ) )
131 130 xnegeqi ⊢ -𝑒 ( lim sup ‘ ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ) = -𝑒 ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑥 ) ) )
132 131 a1i ⊢ ( 𝜑 → -𝑒 ( lim sup ‘ ( 𝑦 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑦 ) ) ) = -𝑒 ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑥 ) ) ) )
133 122 132 eqtrd ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = -𝑒 ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 ( 𝐹 ‘ 𝑥 ) ) ) )