Metamath Proof Explorer

Theorem supcnvlimsup

Description: If a function on a set of upper integers has a real superior limit, the supremum of the rightmost parts of the function, converges to that superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses supcnvlimsup.m 
|- ( ph -> M e. ZZ )
supcnvlimsup.z 
|- Z = ( ZZ>= ` M )
supcnvlimsup.f 
|- ( ph -> F : Z --> RR )
supcnvlimsup.r 
|- ( ph -> ( limsup ` F ) e. RR )
Assertion supcnvlimsup 
|- ( ph -> ( k e. Z |-> sup ( ran ( F |` ( ZZ>= ` k ) ) , RR* , < ) ) ~~> ( limsup ` F ) )

Proof

Step Hyp Ref Expression
1 supcnvlimsup.m 
 |-  ( ph -> M e. ZZ )
2 supcnvlimsup.z 
 |-  Z = ( ZZ>= ` M )
3 supcnvlimsup.f 
 |-  ( ph -> F : Z --> RR )
4 supcnvlimsup.r 
 |-  ( ph -> ( limsup ` F ) e. RR )
5 3 adantr 
 |-  ( ( ph /\ n e. Z ) -> F : Z --> RR )
6 id 
 |-  ( n e. Z -> n e. Z )
7 2 6 uzssd2 
 |-  ( n e. Z -> ( ZZ>= ` n ) C_ Z )
8 7 adantl 
 |-  ( ( ph /\ n e. Z ) -> ( ZZ>= ` n ) C_ Z )
9 5 8 feqresmpt 
 |-  ( ( ph /\ n e. Z ) -> ( F |` ( ZZ>= ` n ) ) = ( m e. ( ZZ>= ` n ) |-> ( F ` m ) ) )
10 9 rneqd 
 |-  ( ( ph /\ n e. Z ) -> ran ( F |` ( ZZ>= ` n ) ) = ran ( m e. ( ZZ>= ` n ) |-> ( F ` m ) ) )
11 10 supeq1d 
 |-  ( ( ph /\ n e. Z ) -> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) = sup ( ran ( m e. ( ZZ>= ` n ) |-> ( F ` m ) ) , RR* , < ) )
12 nfcv 
 |-  F/_ m F
13 4 renepnfd 
 |-  ( ph -> ( limsup ` F ) =/= +oo )
14 12 2 3 13 limsupubuz 
 |-  ( ph -> E. x e. RR A. m e. Z ( F ` m ) <_ x )
15 14 adantr 
 |-  ( ( ph /\ n e. Z ) -> E. x e. RR A. m e. Z ( F ` m ) <_ x )
16 ssralv 
 |-  ( ( ZZ>= ` n ) C_ Z -> ( A. m e. Z ( F ` m ) <_ x -> A. m e. ( ZZ>= ` n ) ( F ` m ) <_ x ) )
17 7 16 syl 
 |-  ( n e. Z -> ( A. m e. Z ( F ` m ) <_ x -> A. m e. ( ZZ>= ` n ) ( F ` m ) <_ x ) )
18 17 adantl 
 |-  ( ( ph /\ n e. Z ) -> ( A. m e. Z ( F ` m ) <_ x -> A. m e. ( ZZ>= ` n ) ( F ` m ) <_ x ) )
19 18 reximdv 
 |-  ( ( ph /\ n e. Z ) -> ( E. x e. RR A. m e. Z ( F ` m ) <_ x -> E. x e. RR A. m e. ( ZZ>= ` n ) ( F ` m ) <_ x ) )
20 15 19 mpd 
 |-  ( ( ph /\ n e. Z ) -> E. x e. RR A. m e. ( ZZ>= ` n ) ( F ` m ) <_ x )
21 nfv 
 |-  F/ m ( ph /\ n e. Z )
22 2 eluzelz2 
 |-  ( n e. Z -> n e. ZZ )
23 uzid 
 |-  ( n e. ZZ -> n e. ( ZZ>= ` n ) )
24 ne0i 
 |-  ( n e. ( ZZ>= ` n ) -> ( ZZ>= ` n ) =/= (/) )
25 22 23 24 3syl 
 |-  ( n e. Z -> ( ZZ>= ` n ) =/= (/) )
26 25 adantl 
 |-  ( ( ph /\ n e. Z ) -> ( ZZ>= ` n ) =/= (/) )
27 5 adantr 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> F : Z --> RR )
28 8 sselda 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> m e. Z )
29 27 28 ffvelrnd 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> ( F ` m ) e. RR )
30 21 26 29 supxrre3rnmpt 
 |-  ( ( ph /\ n e. Z ) -> ( sup ( ran ( m e. ( ZZ>= ` n ) |-> ( F ` m ) ) , RR* , < ) e. RR <-> E. x e. RR A. m e. ( ZZ>= ` n ) ( F ` m ) <_ x ) )
31 20 30 mpbird 
 |-  ( ( ph /\ n e. Z ) -> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( F ` m ) ) , RR* , < ) e. RR )
32 11 31 eqeltrd 
 |-  ( ( ph /\ n e. Z ) -> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) e. RR )
33 32 fmpttd 
 |-  ( ph -> ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) : Z --> RR )
34 eqid 
 |-  ( ZZ>= ` i ) = ( ZZ>= ` i )
35 2 eluzelz2 
 |-  ( i e. Z -> i e. ZZ )
36 35 peano2zd 
 |-  ( i e. Z -> ( i + 1 ) e. ZZ )
37 35 zred 
 |-  ( i e. Z -> i e. RR )
38 lep1 
 |-  ( i e. RR -> i <_ ( i + 1 ) )
39 37 38 syl 
 |-  ( i e. Z -> i <_ ( i + 1 ) )
40 34 35 36 39 eluzd 
 |-  ( i e. Z -> ( i + 1 ) e. ( ZZ>= ` i ) )
41 uzss 
 |-  ( ( i + 1 ) e. ( ZZ>= ` i ) -> ( ZZ>= ` ( i + 1 ) ) C_ ( ZZ>= ` i ) )
42 40 41 syl 
 |-  ( i e. Z -> ( ZZ>= ` ( i + 1 ) ) C_ ( ZZ>= ` i ) )
43 ssres2 
 |-  ( ( ZZ>= ` ( i + 1 ) ) C_ ( ZZ>= ` i ) -> ( F |` ( ZZ>= ` ( i + 1 ) ) ) C_ ( F |` ( ZZ>= ` i ) ) )
44 42 43 syl 
 |-  ( i e. Z -> ( F |` ( ZZ>= ` ( i + 1 ) ) ) C_ ( F |` ( ZZ>= ` i ) ) )
45 rnss 
 |-  ( ( F |` ( ZZ>= ` ( i + 1 ) ) ) C_ ( F |` ( ZZ>= ` i ) ) -> ran ( F |` ( ZZ>= ` ( i + 1 ) ) ) C_ ran ( F |` ( ZZ>= ` i ) ) )
46 44 45 syl 
 |-  ( i e. Z -> ran ( F |` ( ZZ>= ` ( i + 1 ) ) ) C_ ran ( F |` ( ZZ>= ` i ) ) )
47 46 adantl 
 |-  ( ( ph /\ i e. Z ) -> ran ( F |` ( ZZ>= ` ( i + 1 ) ) ) C_ ran ( F |` ( ZZ>= ` i ) ) )
48 rnresss 
 |-  ran ( F |` ( ZZ>= ` i ) ) C_ ran F
49 48 a1i 
 |-  ( ( ph /\ i e. Z ) -> ran ( F |` ( ZZ>= ` i ) ) C_ ran F )
50 3 frnd 
 |-  ( ph -> ran F C_ RR )
51 50 adantr 
 |-  ( ( ph /\ i e. Z ) -> ran F C_ RR )
52 49 51 sstrd 
 |-  ( ( ph /\ i e. Z ) -> ran ( F |` ( ZZ>= ` i ) ) C_ RR )
53 ressxr 
 |-  RR C_ RR*
54 53 a1i 
 |-  ( ( ph /\ i e. Z ) -> RR C_ RR* )
55 52 54 sstrd 
 |-  ( ( ph /\ i e. Z ) -> ran ( F |` ( ZZ>= ` i ) ) C_ RR* )
56 supxrss 
 |-  ( ( ran ( F |` ( ZZ>= ` ( i + 1 ) ) ) C_ ran ( F |` ( ZZ>= ` i ) ) /\ ran ( F |` ( ZZ>= ` i ) ) C_ RR* ) -> sup ( ran ( F |` ( ZZ>= ` ( i + 1 ) ) ) , RR* , < ) <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
57 47 55 56 syl2anc 
 |-  ( ( ph /\ i e. Z ) -> sup ( ran ( F |` ( ZZ>= ` ( i + 1 ) ) ) , RR* , < ) <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
58 eqidd 
 |-  ( i e. Z -> ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) = ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) )
59 fveq2 
 |-  ( n = ( i + 1 ) -> ( ZZ>= ` n ) = ( ZZ>= ` ( i + 1 ) ) )
60 59 reseq2d 
 |-  ( n = ( i + 1 ) -> ( F |` ( ZZ>= ` n ) ) = ( F |` ( ZZ>= ` ( i + 1 ) ) ) )
61 60 rneqd 
 |-  ( n = ( i + 1 ) -> ran ( F |` ( ZZ>= ` n ) ) = ran ( F |` ( ZZ>= ` ( i + 1 ) ) ) )
62 61 supeq1d 
 |-  ( n = ( i + 1 ) -> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` ( i + 1 ) ) ) , RR* , < ) )
63 62 adantl 
 |-  ( ( i e. Z /\ n = ( i + 1 ) ) -> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` ( i + 1 ) ) ) , RR* , < ) )
64 2 peano2uzs 
 |-  ( i e. Z -> ( i + 1 ) e. Z )
65 xrltso 
 |-  < Or RR*
66 65 supex 
 |-  sup ( ran ( F |` ( ZZ>= ` ( i + 1 ) ) ) , RR* , < ) e. _V
67 66 a1i 
 |-  ( i e. Z -> sup ( ran ( F |` ( ZZ>= ` ( i + 1 ) ) ) , RR* , < ) e. _V )
68 58 63 64 67 fvmptd 
 |-  ( i e. Z -> ( ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) ` ( i + 1 ) ) = sup ( ran ( F |` ( ZZ>= ` ( i + 1 ) ) ) , RR* , < ) )
69 68 adantl 
 |-  ( ( ph /\ i e. Z ) -> ( ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) ` ( i + 1 ) ) = sup ( ran ( F |` ( ZZ>= ` ( i + 1 ) ) ) , RR* , < ) )
70 fveq2 
 |-  ( n = i -> ( ZZ>= ` n ) = ( ZZ>= ` i ) )
71 70 reseq2d 
 |-  ( n = i -> ( F |` ( ZZ>= ` n ) ) = ( F |` ( ZZ>= ` i ) ) )
72 71 rneqd 
 |-  ( n = i -> ran ( F |` ( ZZ>= ` n ) ) = ran ( F |` ( ZZ>= ` i ) ) )
73 72 supeq1d 
 |-  ( n = i -> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
74 73 adantl 
 |-  ( ( i e. Z /\ n = i ) -> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
75 id 
 |-  ( i e. Z -> i e. Z )
76 65 supex 
 |-  sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) e. _V
77 76 a1i 
 |-  ( i e. Z -> sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) e. _V )
78 58 74 75 77 fvmptd 
 |-  ( i e. Z -> ( ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) ` i ) = sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
79 78 adantl 
 |-  ( ( ph /\ i e. Z ) -> ( ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) ` i ) = sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
80 69 79 breq12d 
 |-  ( ( ph /\ i e. Z ) -> ( ( ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) ` ( i + 1 ) ) <_ ( ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) ` i ) <-> sup ( ran ( F |` ( ZZ>= ` ( i + 1 ) ) ) , RR* , < ) <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) ) )
81 57 80 mpbird 
 |-  ( ( ph /\ i e. Z ) -> ( ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) ` ( i + 1 ) ) <_ ( ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) ` i ) )
82 nfcv 
 |-  F/_ j F
83 3 frexr 
 |-  ( ph -> F : Z --> RR* )
84 82 1 2 83 limsupre3uz 
 |-  ( ph -> ( ( limsup ` F ) e. RR <-> ( E. x e. RR A. i e. Z E. j e. ( ZZ>= ` i ) x <_ ( F ` j ) /\ E. x e. RR E. i e. Z A. j e. ( ZZ>= ` i ) ( F ` j ) <_ x ) ) )
85 4 84 mpbid 
 |-  ( ph -> ( E. x e. RR A. i e. Z E. j e. ( ZZ>= ` i ) x <_ ( F ` j ) /\ E. x e. RR E. i e. Z A. j e. ( ZZ>= ` i ) ( F ` j ) <_ x ) )
86 85 simpld 
 |-  ( ph -> E. x e. RR A. i e. Z E. j e. ( ZZ>= ` i ) x <_ ( F ` j ) )
87 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> x e. RR )
88 87 rexrd 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> x e. RR* )
89 83 3ad2ant1 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> F : Z --> RR* )
90 2 uztrn2 
 |-  ( ( i e. Z /\ j e. ( ZZ>= ` i ) ) -> j e. Z )
91 90 3adant1 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> j e. Z )
92 89 91 ffvelrnd 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ( F ` j ) e. RR* )
93 92 ad5ant134 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> ( F ` j ) e. RR* )
94 55 supxrcld 
 |-  ( ( ph /\ i e. Z ) -> sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) e. RR* )
95 94 ad5ant13 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) e. RR* )
96 simpr 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> x <_ ( F ` j ) )
97 55 3adant3 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ran ( F |` ( ZZ>= ` i ) ) C_ RR* )
98 fvres 
 |-  ( j e. ( ZZ>= ` i ) -> ( ( F |` ( ZZ>= ` i ) ) ` j ) = ( F ` j ) )
99 98 eqcomd 
 |-  ( j e. ( ZZ>= ` i ) -> ( F ` j ) = ( ( F |` ( ZZ>= ` i ) ) ` j ) )
100 99 3ad2ant3 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ( F ` j ) = ( ( F |` ( ZZ>= ` i ) ) ` j ) )
101 3 ffnd 
 |-  ( ph -> F Fn Z )
102 101 adantr 
 |-  ( ( ph /\ i e. Z ) -> F Fn Z )
103 2 75 uzssd2 
 |-  ( i e. Z -> ( ZZ>= ` i ) C_ Z )
104 103 adantl 
 |-  ( ( ph /\ i e. Z ) -> ( ZZ>= ` i ) C_ Z )
105 fnssres 
 |-  ( ( F Fn Z /\ ( ZZ>= ` i ) C_ Z ) -> ( F |` ( ZZ>= ` i ) ) Fn ( ZZ>= ` i ) )
106 102 104 105 syl2anc 
 |-  ( ( ph /\ i e. Z ) -> ( F |` ( ZZ>= ` i ) ) Fn ( ZZ>= ` i ) )
107 106 3adant3 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ( F |` ( ZZ>= ` i ) ) Fn ( ZZ>= ` i ) )
108 simp3 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> j e. ( ZZ>= ` i ) )
109 fnfvelrn 
 |-  ( ( ( F |` ( ZZ>= ` i ) ) Fn ( ZZ>= ` i ) /\ j e. ( ZZ>= ` i ) ) -> ( ( F |` ( ZZ>= ` i ) ) ` j ) e. ran ( F |` ( ZZ>= ` i ) ) )
110 107 108 109 syl2anc 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ( ( F |` ( ZZ>= ` i ) ) ` j ) e. ran ( F |` ( ZZ>= ` i ) ) )
111 100 110 eqeltrd 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ( F ` j ) e. ran ( F |` ( ZZ>= ` i ) ) )
112 eqid 
 |-  sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < )
113 97 111 112 supxrubd 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ( F ` j ) <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
114 113 ad5ant134 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> ( F ` j ) <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
115 88 93 95 96 114 xrletrd 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> x <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
116 115 rexlimdva2 
 |-  ( ( ( ph /\ x e. RR ) /\ i e. Z ) -> ( E. j e. ( ZZ>= ` i ) x <_ ( F ` j ) -> x <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) ) )
117 116 ralimdva 
 |-  ( ( ph /\ x e. RR ) -> ( A. i e. Z E. j e. ( ZZ>= ` i ) x <_ ( F ` j ) -> A. i e. Z x <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) ) )
118 117 reximdva 
 |-  ( ph -> ( E. x e. RR A. i e. Z E. j e. ( ZZ>= ` i ) x <_ ( F ` j ) -> E. x e. RR A. i e. Z x <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) ) )
119 86 118 mpd 
 |-  ( ph -> E. x e. RR A. i e. Z x <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
120 simpl 
 |-  ( ( y = x /\ i e. Z ) -> y = x )
121 78 adantl 
 |-  ( ( y = x /\ i e. Z ) -> ( ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) ` i ) = sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
122 120 121 breq12d 
 |-  ( ( y = x /\ i e. Z ) -> ( y <_ ( ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) ` i ) <-> x <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) ) )
123 122 ralbidva 
 |-  ( y = x -> ( A. i e. Z y <_ ( ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) ` i ) <-> A. i e. Z x <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) ) )
124 123 cbvrexvw 
 |-  ( E. y e. RR A. i e. Z y <_ ( ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) ` i ) <-> E. x e. RR A. i e. Z x <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
125 119 124 sylibr 
 |-  ( ph -> E. y e. RR A. i e. Z y <_ ( ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) ` i ) )
126 2 1 33 81 125 climinf 
 |-  ( ph -> ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) ~~> inf ( ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) , RR , < ) )
127 fveq2 
 |-  ( n = k -> ( ZZ>= ` n ) = ( ZZ>= ` k ) )
128 127 reseq2d 
 |-  ( n = k -> ( F |` ( ZZ>= ` n ) ) = ( F |` ( ZZ>= ` k ) ) )
129 128 rneqd 
 |-  ( n = k -> ran ( F |` ( ZZ>= ` n ) ) = ran ( F |` ( ZZ>= ` k ) ) )
130 129 supeq1d 
 |-  ( n = k -> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` k ) ) , RR* , < ) )
131 130 cbvmptv 
 |-  ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) = ( k e. Z |-> sup ( ran ( F |` ( ZZ>= ` k ) ) , RR* , < ) )
132 131 a1i 
 |-  ( ph -> ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) = ( k e. Z |-> sup ( ran ( F |` ( ZZ>= ` k ) ) , RR* , < ) ) )
133 1 2 3 4 limsupvaluz2 
 |-  ( ph -> ( limsup ` F ) = inf ( ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) , RR , < ) )
134 133 eqcomd 
 |-  ( ph -> inf ( ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) , RR , < ) = ( limsup ` F ) )
135 132 134 breq12d 
 |-  ( ph -> ( ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) ~~> inf ( ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) , RR , < ) <-> ( k e. Z |-> sup ( ran ( F |` ( ZZ>= ` k ) ) , RR* , < ) ) ~~> ( limsup ` F ) ) )
136 126 135 mpbid 
 |-  ( ph -> ( k e. Z |-> sup ( ran ( F |` ( ZZ>= ` k ) ) , RR* , < ) ) ~~> ( limsup ` F ) )