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 ffvelcdmd 
 |-  ( ( ( 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 ssres2 
 |-  ( ( ZZ>= ` ( i + 1 ) ) C_ ( ZZ>= ` i ) -> ( F |` ( ZZ>= ` ( i + 1 ) ) ) C_ ( F |` ( ZZ>= ` i ) ) )
43 rnss 
 |-  ( ( F |` ( ZZ>= ` ( i + 1 ) ) ) C_ ( F |` ( ZZ>= ` i ) ) -> ran ( F |` ( ZZ>= ` ( i + 1 ) ) ) C_ ran ( F |` ( ZZ>= ` i ) ) )
44 40 41 42 43 4syl 
 |-  ( i e. Z -> ran ( F |` ( ZZ>= ` ( i + 1 ) ) ) C_ ran ( F |` ( ZZ>= ` i ) ) )
45 44 adantl 
 |-  ( ( ph /\ i e. Z ) -> ran ( F |` ( ZZ>= ` ( i + 1 ) ) ) C_ ran ( F |` ( ZZ>= ` i ) ) )
46 rnresss 
 |-  ran ( F |` ( ZZ>= ` i ) ) C_ ran F
47 46 a1i 
 |-  ( ( ph /\ i e. Z ) -> ran ( F |` ( ZZ>= ` i ) ) C_ ran F )
48 3 frnd 
 |-  ( ph -> ran F C_ RR )
49 48 adantr 
 |-  ( ( ph /\ i e. Z ) -> ran F C_ RR )
50 47 49 sstrd 
 |-  ( ( ph /\ i e. Z ) -> ran ( F |` ( ZZ>= ` i ) ) C_ RR )
51 ressxr 
 |-  RR C_ RR*
52 51 a1i 
 |-  ( ( ph /\ i e. Z ) -> RR C_ RR* )
53 50 52 sstrd 
 |-  ( ( ph /\ i e. Z ) -> ran ( F |` ( ZZ>= ` i ) ) C_ RR* )
54 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* , < ) )
55 45 53 54 syl2anc 
 |-  ( ( ph /\ i e. Z ) -> sup ( ran ( F |` ( ZZ>= ` ( i + 1 ) ) ) , RR* , < ) <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
56 eqidd 
 |-  ( i e. Z -> ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) = ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) )
57 fveq2 
 |-  ( n = ( i + 1 ) -> ( ZZ>= ` n ) = ( ZZ>= ` ( i + 1 ) ) )
58 57 reseq2d 
 |-  ( n = ( i + 1 ) -> ( F |` ( ZZ>= ` n ) ) = ( F |` ( ZZ>= ` ( i + 1 ) ) ) )
59 58 rneqd 
 |-  ( n = ( i + 1 ) -> ran ( F |` ( ZZ>= ` n ) ) = ran ( F |` ( ZZ>= ` ( i + 1 ) ) ) )
60 59 supeq1d 
 |-  ( n = ( i + 1 ) -> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` ( i + 1 ) ) ) , RR* , < ) )
61 60 adantl 
 |-  ( ( i e. Z /\ n = ( i + 1 ) ) -> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` ( i + 1 ) ) ) , RR* , < ) )
62 2 peano2uzs 
 |-  ( i e. Z -> ( i + 1 ) e. Z )
63 xrltso 
 |-  < Or RR*
64 63 supex 
 |-  sup ( ran ( F |` ( ZZ>= ` ( i + 1 ) ) ) , RR* , < ) e. _V
65 64 a1i 
 |-  ( i e. Z -> sup ( ran ( F |` ( ZZ>= ` ( i + 1 ) ) ) , RR* , < ) e. _V )
66 56 61 62 65 fvmptd 
 |-  ( i e. Z -> ( ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) ` ( i + 1 ) ) = sup ( ran ( F |` ( ZZ>= ` ( i + 1 ) ) ) , RR* , < ) )
67 66 adantl 
 |-  ( ( ph /\ i e. Z ) -> ( ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) ` ( i + 1 ) ) = sup ( ran ( F |` ( ZZ>= ` ( i + 1 ) ) ) , RR* , < ) )
68 fveq2 
 |-  ( n = i -> ( ZZ>= ` n ) = ( ZZ>= ` i ) )
69 68 reseq2d 
 |-  ( n = i -> ( F |` ( ZZ>= ` n ) ) = ( F |` ( ZZ>= ` i ) ) )
70 69 rneqd 
 |-  ( n = i -> ran ( F |` ( ZZ>= ` n ) ) = ran ( F |` ( ZZ>= ` i ) ) )
71 70 supeq1d 
 |-  ( n = i -> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
72 71 adantl 
 |-  ( ( i e. Z /\ n = i ) -> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
73 id 
 |-  ( i e. Z -> i e. Z )
74 63 supex 
 |-  sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) e. _V
75 74 a1i 
 |-  ( i e. Z -> sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) e. _V )
76 56 72 73 75 fvmptd 
 |-  ( i e. Z -> ( ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) ` i ) = sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
77 76 adantl 
 |-  ( ( ph /\ i e. Z ) -> ( ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) ` i ) = sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
78 67 77 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* , < ) ) )
79 55 78 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 ) )
80 nfcv 
 |-  F/_ j F
81 3 frexr 
 |-  ( ph -> F : Z --> RR* )
82 80 1 2 81 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 ) ) )
83 4 82 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 ) )
84 83 simpld 
 |-  ( ph -> E. x e. RR A. i e. Z E. j e. ( ZZ>= ` i ) x <_ ( F ` j ) )
85 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> x e. RR )
86 85 rexrd 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> x e. RR* )
87 81 3ad2ant1 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> F : Z --> RR* )
88 2 uztrn2 
 |-  ( ( i e. Z /\ j e. ( ZZ>= ` i ) ) -> j e. Z )
89 88 3adant1 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> j e. Z )
90 87 89 ffvelcdmd 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ( F ` j ) e. RR* )
91 90 ad5ant134 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> ( F ` j ) e. RR* )
92 53 supxrcld 
 |-  ( ( ph /\ i e. Z ) -> sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) e. RR* )
93 92 ad5ant13 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) e. RR* )
94 simpr 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> x <_ ( F ` j ) )
95 53 3adant3 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ran ( F |` ( ZZ>= ` i ) ) C_ RR* )
96 fvres 
 |-  ( j e. ( ZZ>= ` i ) -> ( ( F |` ( ZZ>= ` i ) ) ` j ) = ( F ` j ) )
97 96 eqcomd 
 |-  ( j e. ( ZZ>= ` i ) -> ( F ` j ) = ( ( F |` ( ZZ>= ` i ) ) ` j ) )
98 97 3ad2ant3 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ( F ` j ) = ( ( F |` ( ZZ>= ` i ) ) ` j ) )
99 3 ffnd 
 |-  ( ph -> F Fn Z )
100 99 adantr 
 |-  ( ( ph /\ i e. Z ) -> F Fn Z )
101 2 73 uzssd2 
 |-  ( i e. Z -> ( ZZ>= ` i ) C_ Z )
102 101 adantl 
 |-  ( ( ph /\ i e. Z ) -> ( ZZ>= ` i ) C_ Z )
103 fnssres 
 |-  ( ( F Fn Z /\ ( ZZ>= ` i ) C_ Z ) -> ( F |` ( ZZ>= ` i ) ) Fn ( ZZ>= ` i ) )
104 100 102 103 syl2anc 
 |-  ( ( ph /\ i e. Z ) -> ( F |` ( ZZ>= ` i ) ) Fn ( ZZ>= ` i ) )
105 104 3adant3 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ( F |` ( ZZ>= ` i ) ) Fn ( ZZ>= ` i ) )
106 simp3 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> j e. ( ZZ>= ` i ) )
107 fnfvelrn 
 |-  ( ( ( F |` ( ZZ>= ` i ) ) Fn ( ZZ>= ` i ) /\ j e. ( ZZ>= ` i ) ) -> ( ( F |` ( ZZ>= ` i ) ) ` j ) e. ran ( F |` ( ZZ>= ` i ) ) )
108 105 106 107 syl2anc 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ( ( F |` ( ZZ>= ` i ) ) ` j ) e. ran ( F |` ( ZZ>= ` i ) ) )
109 98 108 eqeltrd 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ( F ` j ) e. ran ( F |` ( ZZ>= ` i ) ) )
110 eqid 
 |-  sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < )
111 95 109 110 supxrubd 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ( F ` j ) <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
112 111 ad5ant134 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> ( F ` j ) <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
113 86 91 93 94 112 xrletrd 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> x <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
114 113 rexlimdva2 
 |-  ( ( ( ph /\ x e. RR ) /\ i e. Z ) -> ( E. j e. ( ZZ>= ` i ) x <_ ( F ` j ) -> x <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) ) )
115 114 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* , < ) ) )
116 115 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* , < ) ) )
117 84 116 mpd 
 |-  ( ph -> E. x e. RR A. i e. Z x <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
118 simpl 
 |-  ( ( y = x /\ i e. Z ) -> y = x )
119 76 adantl 
 |-  ( ( y = x /\ i e. Z ) -> ( ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) ` i ) = sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
120 118 119 breq12d 
 |-  ( ( y = x /\ i e. Z ) -> ( y <_ ( ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) ` i ) <-> x <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) ) )
121 120 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* , < ) ) )
122 121 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* , < ) )
123 117 122 sylibr 
 |-  ( ph -> E. y e. RR A. i e. Z y <_ ( ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) ` i ) )
124 2 1 33 79 123 climinf 
 |-  ( ph -> ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) ~~> inf ( ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) , RR , < ) )
125 fveq2 
 |-  ( n = k -> ( ZZ>= ` n ) = ( ZZ>= ` k ) )
126 125 reseq2d 
 |-  ( n = k -> ( F |` ( ZZ>= ` n ) ) = ( F |` ( ZZ>= ` k ) ) )
127 126 rneqd 
 |-  ( n = k -> ran ( F |` ( ZZ>= ` n ) ) = ran ( F |` ( ZZ>= ` k ) ) )
128 127 supeq1d 
 |-  ( n = k -> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` k ) ) , RR* , < ) )
129 128 cbvmptv 
 |-  ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) = ( k e. Z |-> sup ( ran ( F |` ( ZZ>= ` k ) ) , RR* , < ) )
130 129 a1i 
 |-  ( ph -> ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) = ( k e. Z |-> sup ( ran ( F |` ( ZZ>= ` k ) ) , RR* , < ) ) )
131 1 2 3 4 limsupvaluz2 
 |-  ( ph -> ( limsup ` F ) = inf ( ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) , RR , < ) )
132 131 eqcomd 
 |-  ( ph -> inf ( ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) , RR , < ) = ( limsup ` F ) )
133 130 132 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 ) ) )
134 124 133 mpbid 
 |-  ( ph -> ( k e. Z |-> sup ( ran ( F |` ( ZZ>= ` k ) ) , RR* , < ) ) ~~> ( limsup ` F ) )