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 
|- F/_ x F
liminfvalxr.2 
|- ( ph -> A e. V )
liminfvalxr.3 
|- ( ph -> F : A --> RR* )
Assertion liminfvalxr 
|- ( ph -> ( liminf ` F ) = -e ( limsup ` ( x e. A |-> -e ( F ` x ) ) ) )

Proof

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