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

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 biimpi 
 |-  ( -e ( F ` y ) = -e z -> -e z = -e ( F ` y ) )
41 40 adantl 
 |-  ( ( ( ( ph /\ z e. RR* ) /\ y e. ( A i^i ( k [,) +oo ) ) ) /\ -e ( F ` y ) = -e z ) -> -e z = -e ( F ` y ) )
42 simplr 
 |-  ( ( ( ph /\ z e. RR* ) /\ y e. ( A i^i ( k [,) +oo ) ) ) -> z e. RR* )
43 3 adantr 
 |-  ( ( ph /\ y e. ( A i^i ( k [,) +oo ) ) ) -> F : A --> RR* )
44 30 adantl 
 |-  ( ( ph /\ y e. ( A i^i ( k [,) +oo ) ) ) -> y e. A )
45 43 44 ffvelcdmd 
 |-  ( ( ph /\ y e. ( A i^i ( k [,) +oo ) ) ) -> ( F ` y ) e. RR* )
46 45 adantlr 
 |-  ( ( ( ph /\ z e. RR* ) /\ y e. ( A i^i ( k [,) +oo ) ) ) -> ( F ` y ) e. RR* )
47 xneg11 
 |-  ( ( z e. RR* /\ ( F ` y ) e. RR* ) -> ( -e z = -e ( F ` y ) <-> z = ( F ` y ) ) )
48 42 46 47 syl2anc 
 |-  ( ( ( ph /\ z e. RR* ) /\ y e. ( A i^i ( k [,) +oo ) ) ) -> ( -e z = -e ( F ` y ) <-> z = ( F ` y ) ) )
49 48 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 ) ) )
50 41 49 mpbid 
 |-  ( ( ( ( ph /\ z e. RR* ) /\ y e. ( A i^i ( k [,) +oo ) ) ) /\ -e ( F ` y ) = -e z ) -> z = ( F ` y ) )
51 3 ffund 
 |-  ( ph -> Fun F )
52 51 30 anim12i 
 |-  ( ( ph /\ y e. ( A i^i ( k [,) +oo ) ) ) -> ( Fun F /\ y e. A ) )
53 52 simpld 
 |-  ( ( ph /\ y e. ( A i^i ( k [,) +oo ) ) ) -> Fun F )
54 3 fdmd 
 |-  ( ph -> dom F = A )
55 54 eqcomd 
 |-  ( ph -> A = dom F )
56 55 adantr 
 |-  ( ( ph /\ y e. ( A i^i ( k [,) +oo ) ) ) -> A = dom F )
57 44 56 eleqtrd 
 |-  ( ( ph /\ y e. ( A i^i ( k [,) +oo ) ) ) -> y e. dom F )
58 53 57 jca 
 |-  ( ( ph /\ y e. ( A i^i ( k [,) +oo ) ) ) -> ( Fun F /\ y e. dom F ) )
59 elinel2 
 |-  ( y e. ( A i^i ( k [,) +oo ) ) -> y e. ( k [,) +oo ) )
60 59 adantl 
 |-  ( ( ph /\ y e. ( A i^i ( k [,) +oo ) ) ) -> y e. ( k [,) +oo ) )
61 funfvima 
 |-  ( ( Fun F /\ y e. dom F ) -> ( y e. ( k [,) +oo ) -> ( F ` y ) e. ( F " ( k [,) +oo ) ) ) )
62 58 60 61 sylc 
 |-  ( ( ph /\ y e. ( A i^i ( k [,) +oo ) ) ) -> ( F ` y ) e. ( F " ( k [,) +oo ) ) )
63 62 ad4ant13 
 |-  ( ( ( ( ph /\ z e. RR* ) /\ y e. ( A i^i ( k [,) +oo ) ) ) /\ -e ( F ` y ) = -e z ) -> ( F ` y ) e. ( F " ( k [,) +oo ) ) )
64 50 63 eqeltrd 
 |-  ( ( ( ( ph /\ z e. RR* ) /\ y e. ( A i^i ( k [,) +oo ) ) ) /\ -e ( F ` y ) = -e z ) -> z e. ( F " ( k [,) +oo ) ) )
65 38 64 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 ) ) )
66 65 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 ) ) ) )
67 66 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 ) ) ) )
68 29 67 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 ) ) ) )
69 28 68 mpd 
 |-  ( ( ph /\ z e. RR* /\ -e z e. ( ( ( y e. A |-> -e ( F ` y ) ) " ( k [,) +oo ) ) i^i RR* ) ) -> z e. ( F " ( k [,) +oo ) ) )
70 69 rabssdv 
 |-  ( ph -> { z e. RR* | -e z e. ( ( ( y e. A |-> -e ( F ` y ) ) " ( k [,) +oo ) ) i^i RR* ) } C_ ( F " ( k [,) +oo ) ) )
71 ssrab2 
 |-  { z e. RR* | -e z e. ( ( ( y e. A |-> -e ( F ` y ) ) " ( k [,) +oo ) ) i^i RR* ) } C_ RR*
72 71 a1i 
 |-  ( ph -> { z e. RR* | -e z e. ( ( ( y e. A |-> -e ( F ` y ) ) " ( k [,) +oo ) ) i^i RR* ) } C_ RR* )
73 70 72 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* ) )
74 5 a1i 
 |-  ( ph -> ( ( F " ( k [,) +oo ) ) i^i RR* ) C_ RR* )
75 3 ffnd 
 |-  ( ph -> F Fn A )
76 75 adantr 
 |-  ( ( ph /\ z e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) -> F Fn A )
77 elinel1 
 |-  ( z e. ( ( F " ( k [,) +oo ) ) i^i RR* ) -> z e. ( F " ( k [,) +oo ) ) )
78 77 adantl 
 |-  ( ( ph /\ z e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) -> z e. ( F " ( k [,) +oo ) ) )
79 fvelima2 
 |-  ( ( F Fn A /\ z e. ( F " ( k [,) +oo ) ) ) -> E. y e. ( A i^i ( k [,) +oo ) ) ( F ` y ) = z )
80 76 78 79 syl2anc 
 |-  ( ( ph /\ z e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) -> E. y e. ( A i^i ( k [,) +oo ) ) ( F ` y ) = z )
81 elinel2 
 |-  ( z e. ( ( F " ( k [,) +oo ) ) i^i RR* ) -> z e. RR* )
82 eqcom 
 |-  ( ( F ` y ) = z <-> z = ( F ` y ) )
83 82 biimpi 
 |-  ( ( F ` y ) = z -> z = ( F ` y ) )
84 83 adantl 
 |-  ( ( z e. RR* /\ ( F ` y ) = z ) -> z = ( F ` y ) )
85 84 xnegeqd 
 |-  ( ( z e. RR* /\ ( F ` y ) = z ) -> -e z = -e ( F ` y ) )
86 simpl 
 |-  ( ( z e. RR* /\ ( F ` y ) = z ) -> z e. RR* )
87 84 86 eqeltrrd 
 |-  ( ( z e. RR* /\ ( F ` y ) = z ) -> ( F ` y ) e. RR* )
88 86 87 47 syl2anc 
 |-  ( ( z e. RR* /\ ( F ` y ) = z ) -> ( -e z = -e ( F ` y ) <-> z = ( F ` y ) ) )
89 85 88 mpbid 
 |-  ( ( z e. RR* /\ ( F ` y ) = z ) -> z = ( F ` y ) )
90 89 xnegeqd 
 |-  ( ( z e. RR* /\ ( F ` y ) = z ) -> -e z = -e ( F ` y ) )
91 90 ex 
 |-  ( z e. RR* -> ( ( F ` y ) = z -> -e z = -e ( F ` y ) ) )
92 91 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 ) ) )
93 81 92 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 ) ) )
94 93 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 ) ) )
95 80 94 mpd 
 |-  ( ( ph /\ z e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) -> E. y e. ( A i^i ( k [,) +oo ) ) -e z = -e ( F ` y ) )
96 xnegex 
 |-  -e z e. _V
97 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 ) ) )
98 96 97 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 ) )
99 95 98 sylibr 
 |-  ( ( ph /\ z e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) -> -e z e. ( ( y e. A |-> -e ( F ` y ) ) " ( k [,) +oo ) ) )
100 74 sselda 
 |-  ( ( ph /\ z e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) -> z e. RR* )
101 100 xnegcld 
 |-  ( ( ph /\ z e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) -> -e z e. RR* )
102 99 101 elind 
 |-  ( ( ph /\ z e. ( ( F " ( k [,) +oo ) ) i^i RR* ) ) -> -e z e. ( ( ( y e. A |-> -e ( F ` y ) ) " ( k [,) +oo ) ) i^i RR* ) )
103 74 102 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* ) } )
104 73 103 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* ) )
105 104 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* , < ) )
106 105 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* , < ) )
107 17 106 eqtr2d 
 |-  ( ph -> -e inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) = sup ( ( ( ( y e. A |-> -e ( F ` y ) ) " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
108 107 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* , < ) ) )
109 108 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* , < ) ) )
110 109 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* , < ) )
111 110 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* , < ) )
112 11 111 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* , < ) )
113 3 2 fexd 
 |-  ( ph -> F e. _V )
114 eqid 
 |-  ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
115 114 liminfval 
 |-  ( F e. _V -> ( liminf ` F ) = sup ( ran ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
116 113 115 syl 
 |-  ( ph -> ( liminf ` F ) = sup ( ran ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
117 2 mptexd 
 |-  ( ph -> ( y e. A |-> -e ( F ` y ) ) e. _V )
118 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* , < ) )
119 118 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* , < ) )
120 117 119 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* , < ) )
121 120 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* , < ) )
122 112 116 121 3eqtr4d 
 |-  ( ph -> ( liminf ` F ) = -e ( limsup ` ( y e. A |-> -e ( F ` y ) ) ) )
123 nfcv 
 |-  F/_ x y
124 1 123 nffv 
 |-  F/_ x ( F ` y )
125 124 nfxneg 
 |-  F/_ x -e ( F ` y )
126 nfcv 
 |-  F/_ y -e ( F ` x )
127 fveq2 
 |-  ( y = x -> ( F ` y ) = ( F ` x ) )
128 127 xnegeqd 
 |-  ( y = x -> -e ( F ` y ) = -e ( F ` x ) )
129 125 126 128 cbvmpt 
 |-  ( y e. A |-> -e ( F ` y ) ) = ( x e. A |-> -e ( F ` x ) )
130 129 fveq2i 
 |-  ( limsup ` ( y e. A |-> -e ( F ` y ) ) ) = ( limsup ` ( x e. A |-> -e ( F ` x ) ) )
131 130 xnegeqi 
 |-  -e ( limsup ` ( y e. A |-> -e ( F ` y ) ) ) = -e ( limsup ` ( x e. A |-> -e ( F ` x ) ) )
132 131 a1i 
 |-  ( ph -> -e ( limsup ` ( y e. A |-> -e ( F ` y ) ) ) = -e ( limsup ` ( x e. A |-> -e ( F ` x ) ) ) )
133 122 132 eqtrd 
 |-  ( ph -> ( liminf ` F ) = -e ( limsup ` ( x e. A |-> -e ( F ` x ) ) ) )