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 ( 𝜑𝑀 ∈ ℤ )
supcnvlimsup.z 𝑍 = ( ℤ𝑀 )
supcnvlimsup.f ( 𝜑𝐹 : 𝑍 ⟶ ℝ )
supcnvlimsup.r ( 𝜑 → ( lim sup ‘ 𝐹 ) ∈ ℝ )
Assertion supcnvlimsup ( 𝜑 → ( 𝑘𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑘 ) ) , ℝ* , < ) ) ⇝ ( lim sup ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 supcnvlimsup.m ( 𝜑𝑀 ∈ ℤ )
2 supcnvlimsup.z 𝑍 = ( ℤ𝑀 )
3 supcnvlimsup.f ( 𝜑𝐹 : 𝑍 ⟶ ℝ )
4 supcnvlimsup.r ( 𝜑 → ( lim sup ‘ 𝐹 ) ∈ ℝ )
5 3 adantr ( ( 𝜑𝑛𝑍 ) → 𝐹 : 𝑍 ⟶ ℝ )
6 id ( 𝑛𝑍𝑛𝑍 )
7 2 6 uzssd2 ( 𝑛𝑍 → ( ℤ𝑛 ) ⊆ 𝑍 )
8 7 adantl ( ( 𝜑𝑛𝑍 ) → ( ℤ𝑛 ) ⊆ 𝑍 )
9 5 8 feqresmpt ( ( 𝜑𝑛𝑍 ) → ( 𝐹 ↾ ( ℤ𝑛 ) ) = ( 𝑚 ∈ ( ℤ𝑛 ) ↦ ( 𝐹𝑚 ) ) )
10 9 rneqd ( ( 𝜑𝑛𝑍 ) → ran ( 𝐹 ↾ ( ℤ𝑛 ) ) = ran ( 𝑚 ∈ ( ℤ𝑛 ) ↦ ( 𝐹𝑚 ) ) )
11 10 supeq1d ( ( 𝜑𝑛𝑍 ) → sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) = sup ( ran ( 𝑚 ∈ ( ℤ𝑛 ) ↦ ( 𝐹𝑚 ) ) , ℝ* , < ) )
12 nfcv 𝑚 𝐹
13 4 renepnfd ( 𝜑 → ( lim sup ‘ 𝐹 ) ≠ +∞ )
14 12 2 3 13 limsupubuz ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑚𝑍 ( 𝐹𝑚 ) ≤ 𝑥 )
15 14 adantr ( ( 𝜑𝑛𝑍 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑚𝑍 ( 𝐹𝑚 ) ≤ 𝑥 )
16 ssralv ( ( ℤ𝑛 ) ⊆ 𝑍 → ( ∀ 𝑚𝑍 ( 𝐹𝑚 ) ≤ 𝑥 → ∀ 𝑚 ∈ ( ℤ𝑛 ) ( 𝐹𝑚 ) ≤ 𝑥 ) )
17 7 16 syl ( 𝑛𝑍 → ( ∀ 𝑚𝑍 ( 𝐹𝑚 ) ≤ 𝑥 → ∀ 𝑚 ∈ ( ℤ𝑛 ) ( 𝐹𝑚 ) ≤ 𝑥 ) )
18 17 adantl ( ( 𝜑𝑛𝑍 ) → ( ∀ 𝑚𝑍 ( 𝐹𝑚 ) ≤ 𝑥 → ∀ 𝑚 ∈ ( ℤ𝑛 ) ( 𝐹𝑚 ) ≤ 𝑥 ) )
19 18 reximdv ( ( 𝜑𝑛𝑍 ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑚𝑍 ( 𝐹𝑚 ) ≤ 𝑥 → ∃ 𝑥 ∈ ℝ ∀ 𝑚 ∈ ( ℤ𝑛 ) ( 𝐹𝑚 ) ≤ 𝑥 ) )
20 15 19 mpd ( ( 𝜑𝑛𝑍 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑚 ∈ ( ℤ𝑛 ) ( 𝐹𝑚 ) ≤ 𝑥 )
21 nfv 𝑚 ( 𝜑𝑛𝑍 )
22 2 eluzelz2 ( 𝑛𝑍𝑛 ∈ ℤ )
23 uzid ( 𝑛 ∈ ℤ → 𝑛 ∈ ( ℤ𝑛 ) )
24 ne0i ( 𝑛 ∈ ( ℤ𝑛 ) → ( ℤ𝑛 ) ≠ ∅ )
25 22 23 24 3syl ( 𝑛𝑍 → ( ℤ𝑛 ) ≠ ∅ )
26 25 adantl ( ( 𝜑𝑛𝑍 ) → ( ℤ𝑛 ) ≠ ∅ )
27 5 adantr ( ( ( 𝜑𝑛𝑍 ) ∧ 𝑚 ∈ ( ℤ𝑛 ) ) → 𝐹 : 𝑍 ⟶ ℝ )
28 8 sselda ( ( ( 𝜑𝑛𝑍 ) ∧ 𝑚 ∈ ( ℤ𝑛 ) ) → 𝑚𝑍 )
29 27 28 ffvelcdmd ( ( ( 𝜑𝑛𝑍 ) ∧ 𝑚 ∈ ( ℤ𝑛 ) ) → ( 𝐹𝑚 ) ∈ ℝ )
30 21 26 29 supxrre3rnmpt ( ( 𝜑𝑛𝑍 ) → ( sup ( ran ( 𝑚 ∈ ( ℤ𝑛 ) ↦ ( 𝐹𝑚 ) ) , ℝ* , < ) ∈ ℝ ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑚 ∈ ( ℤ𝑛 ) ( 𝐹𝑚 ) ≤ 𝑥 ) )
31 20 30 mpbird ( ( 𝜑𝑛𝑍 ) → sup ( ran ( 𝑚 ∈ ( ℤ𝑛 ) ↦ ( 𝐹𝑚 ) ) , ℝ* , < ) ∈ ℝ )
32 11 31 eqeltrd ( ( 𝜑𝑛𝑍 ) → sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ∈ ℝ )
33 32 fmpttd ( 𝜑 → ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) : 𝑍 ⟶ ℝ )
34 eqid ( ℤ𝑖 ) = ( ℤ𝑖 )
35 2 eluzelz2 ( 𝑖𝑍𝑖 ∈ ℤ )
36 35 peano2zd ( 𝑖𝑍 → ( 𝑖 + 1 ) ∈ ℤ )
37 35 zred ( 𝑖𝑍𝑖 ∈ ℝ )
38 lep1 ( 𝑖 ∈ ℝ → 𝑖 ≤ ( 𝑖 + 1 ) )
39 37 38 syl ( 𝑖𝑍𝑖 ≤ ( 𝑖 + 1 ) )
40 34 35 36 39 eluzd ( 𝑖𝑍 → ( 𝑖 + 1 ) ∈ ( ℤ𝑖 ) )
41 uzss ( ( 𝑖 + 1 ) ∈ ( ℤ𝑖 ) → ( ℤ ‘ ( 𝑖 + 1 ) ) ⊆ ( ℤ𝑖 ) )
42 ssres2 ( ( ℤ ‘ ( 𝑖 + 1 ) ) ⊆ ( ℤ𝑖 ) → ( 𝐹 ↾ ( ℤ ‘ ( 𝑖 + 1 ) ) ) ⊆ ( 𝐹 ↾ ( ℤ𝑖 ) ) )
43 rnss ( ( 𝐹 ↾ ( ℤ ‘ ( 𝑖 + 1 ) ) ) ⊆ ( 𝐹 ↾ ( ℤ𝑖 ) ) → ran ( 𝐹 ↾ ( ℤ ‘ ( 𝑖 + 1 ) ) ) ⊆ ran ( 𝐹 ↾ ( ℤ𝑖 ) ) )
44 40 41 42 43 4syl ( 𝑖𝑍 → ran ( 𝐹 ↾ ( ℤ ‘ ( 𝑖 + 1 ) ) ) ⊆ ran ( 𝐹 ↾ ( ℤ𝑖 ) ) )
45 44 adantl ( ( 𝜑𝑖𝑍 ) → ran ( 𝐹 ↾ ( ℤ ‘ ( 𝑖 + 1 ) ) ) ⊆ ran ( 𝐹 ↾ ( ℤ𝑖 ) ) )
46 rnresss ran ( 𝐹 ↾ ( ℤ𝑖 ) ) ⊆ ran 𝐹
47 46 a1i ( ( 𝜑𝑖𝑍 ) → ran ( 𝐹 ↾ ( ℤ𝑖 ) ) ⊆ ran 𝐹 )
48 3 frnd ( 𝜑 → ran 𝐹 ⊆ ℝ )
49 48 adantr ( ( 𝜑𝑖𝑍 ) → ran 𝐹 ⊆ ℝ )
50 47 49 sstrd ( ( 𝜑𝑖𝑍 ) → ran ( 𝐹 ↾ ( ℤ𝑖 ) ) ⊆ ℝ )
51 ressxr ℝ ⊆ ℝ*
52 51 a1i ( ( 𝜑𝑖𝑍 ) → ℝ ⊆ ℝ* )
53 50 52 sstrd ( ( 𝜑𝑖𝑍 ) → ran ( 𝐹 ↾ ( ℤ𝑖 ) ) ⊆ ℝ* )
54 supxrss ( ( ran ( 𝐹 ↾ ( ℤ ‘ ( 𝑖 + 1 ) ) ) ⊆ ran ( 𝐹 ↾ ( ℤ𝑖 ) ) ∧ ran ( 𝐹 ↾ ( ℤ𝑖 ) ) ⊆ ℝ* ) → sup ( ran ( 𝐹 ↾ ( ℤ ‘ ( 𝑖 + 1 ) ) ) , ℝ* , < ) ≤ sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) )
55 45 53 54 syl2anc ( ( 𝜑𝑖𝑍 ) → sup ( ran ( 𝐹 ↾ ( ℤ ‘ ( 𝑖 + 1 ) ) ) , ℝ* , < ) ≤ sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) )
56 eqidd ( 𝑖𝑍 → ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) = ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) )
57 fveq2 ( 𝑛 = ( 𝑖 + 1 ) → ( ℤ𝑛 ) = ( ℤ ‘ ( 𝑖 + 1 ) ) )
58 57 reseq2d ( 𝑛 = ( 𝑖 + 1 ) → ( 𝐹 ↾ ( ℤ𝑛 ) ) = ( 𝐹 ↾ ( ℤ ‘ ( 𝑖 + 1 ) ) ) )
59 58 rneqd ( 𝑛 = ( 𝑖 + 1 ) → ran ( 𝐹 ↾ ( ℤ𝑛 ) ) = ran ( 𝐹 ↾ ( ℤ ‘ ( 𝑖 + 1 ) ) ) )
60 59 supeq1d ( 𝑛 = ( 𝑖 + 1 ) → sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ ‘ ( 𝑖 + 1 ) ) ) , ℝ* , < ) )
61 60 adantl ( ( 𝑖𝑍𝑛 = ( 𝑖 + 1 ) ) → sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ ‘ ( 𝑖 + 1 ) ) ) , ℝ* , < ) )
62 2 peano2uzs ( 𝑖𝑍 → ( 𝑖 + 1 ) ∈ 𝑍 )
63 xrltso < Or ℝ*
64 63 supex sup ( ran ( 𝐹 ↾ ( ℤ ‘ ( 𝑖 + 1 ) ) ) , ℝ* , < ) ∈ V
65 64 a1i ( 𝑖𝑍 → sup ( ran ( 𝐹 ↾ ( ℤ ‘ ( 𝑖 + 1 ) ) ) , ℝ* , < ) ∈ V )
66 56 61 62 65 fvmptd ( 𝑖𝑍 → ( ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) ‘ ( 𝑖 + 1 ) ) = sup ( ran ( 𝐹 ↾ ( ℤ ‘ ( 𝑖 + 1 ) ) ) , ℝ* , < ) )
67 66 adantl ( ( 𝜑𝑖𝑍 ) → ( ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) ‘ ( 𝑖 + 1 ) ) = sup ( ran ( 𝐹 ↾ ( ℤ ‘ ( 𝑖 + 1 ) ) ) , ℝ* , < ) )
68 fveq2 ( 𝑛 = 𝑖 → ( ℤ𝑛 ) = ( ℤ𝑖 ) )
69 68 reseq2d ( 𝑛 = 𝑖 → ( 𝐹 ↾ ( ℤ𝑛 ) ) = ( 𝐹 ↾ ( ℤ𝑖 ) ) )
70 69 rneqd ( 𝑛 = 𝑖 → ran ( 𝐹 ↾ ( ℤ𝑛 ) ) = ran ( 𝐹 ↾ ( ℤ𝑖 ) ) )
71 70 supeq1d ( 𝑛 = 𝑖 → sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) )
72 71 adantl ( ( 𝑖𝑍𝑛 = 𝑖 ) → sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) )
73 id ( 𝑖𝑍𝑖𝑍 )
74 63 supex sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) ∈ V
75 74 a1i ( 𝑖𝑍 → sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) ∈ V )
76 56 72 73 75 fvmptd ( 𝑖𝑍 → ( ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) ‘ 𝑖 ) = sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) )
77 76 adantl ( ( 𝜑𝑖𝑍 ) → ( ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) ‘ 𝑖 ) = sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) )
78 67 77 breq12d ( ( 𝜑𝑖𝑍 ) → ( ( ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) ‘ ( 𝑖 + 1 ) ) ≤ ( ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) ‘ 𝑖 ) ↔ sup ( ran ( 𝐹 ↾ ( ℤ ‘ ( 𝑖 + 1 ) ) ) , ℝ* , < ) ≤ sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) ) )
79 55 78 mpbird ( ( 𝜑𝑖𝑍 ) → ( ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) ‘ ( 𝑖 + 1 ) ) ≤ ( ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) ‘ 𝑖 ) )
80 nfcv 𝑗 𝐹
81 3 frexr ( 𝜑𝐹 : 𝑍 ⟶ ℝ* )
82 80 1 2 81 limsupre3uz ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) 𝑥 ≤ ( 𝐹𝑗 ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) ( 𝐹𝑗 ) ≤ 𝑥 ) ) )
83 4 82 mpbid ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) 𝑥 ≤ ( 𝐹𝑗 ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) ( 𝐹𝑗 ) ≤ 𝑥 ) )
84 83 simpld ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) 𝑥 ≤ ( 𝐹𝑗 ) )
85 simp-4r ( ( ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑖𝑍 ) ∧ 𝑗 ∈ ( ℤ𝑖 ) ) ∧ 𝑥 ≤ ( 𝐹𝑗 ) ) → 𝑥 ∈ ℝ )
86 85 rexrd ( ( ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑖𝑍 ) ∧ 𝑗 ∈ ( ℤ𝑖 ) ) ∧ 𝑥 ≤ ( 𝐹𝑗 ) ) → 𝑥 ∈ ℝ* )
87 81 3ad2ant1 ( ( 𝜑𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) ) → 𝐹 : 𝑍 ⟶ ℝ* )
88 2 uztrn2 ( ( 𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) ) → 𝑗𝑍 )
89 88 3adant1 ( ( 𝜑𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) ) → 𝑗𝑍 )
90 87 89 ffvelcdmd ( ( 𝜑𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) ) → ( 𝐹𝑗 ) ∈ ℝ* )
91 90 ad5ant134 ( ( ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑖𝑍 ) ∧ 𝑗 ∈ ( ℤ𝑖 ) ) ∧ 𝑥 ≤ ( 𝐹𝑗 ) ) → ( 𝐹𝑗 ) ∈ ℝ* )
92 53 supxrcld ( ( 𝜑𝑖𝑍 ) → sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) ∈ ℝ* )
93 92 ad5ant13 ( ( ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑖𝑍 ) ∧ 𝑗 ∈ ( ℤ𝑖 ) ) ∧ 𝑥 ≤ ( 𝐹𝑗 ) ) → sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) ∈ ℝ* )
94 simpr ( ( ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑖𝑍 ) ∧ 𝑗 ∈ ( ℤ𝑖 ) ) ∧ 𝑥 ≤ ( 𝐹𝑗 ) ) → 𝑥 ≤ ( 𝐹𝑗 ) )
95 53 3adant3 ( ( 𝜑𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) ) → ran ( 𝐹 ↾ ( ℤ𝑖 ) ) ⊆ ℝ* )
96 fvres ( 𝑗 ∈ ( ℤ𝑖 ) → ( ( 𝐹 ↾ ( ℤ𝑖 ) ) ‘ 𝑗 ) = ( 𝐹𝑗 ) )
97 96 eqcomd ( 𝑗 ∈ ( ℤ𝑖 ) → ( 𝐹𝑗 ) = ( ( 𝐹 ↾ ( ℤ𝑖 ) ) ‘ 𝑗 ) )
98 97 3ad2ant3 ( ( 𝜑𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) ) → ( 𝐹𝑗 ) = ( ( 𝐹 ↾ ( ℤ𝑖 ) ) ‘ 𝑗 ) )
99 3 ffnd ( 𝜑𝐹 Fn 𝑍 )
100 99 adantr ( ( 𝜑𝑖𝑍 ) → 𝐹 Fn 𝑍 )
101 2 73 uzssd2 ( 𝑖𝑍 → ( ℤ𝑖 ) ⊆ 𝑍 )
102 101 adantl ( ( 𝜑𝑖𝑍 ) → ( ℤ𝑖 ) ⊆ 𝑍 )
103 fnssres ( ( 𝐹 Fn 𝑍 ∧ ( ℤ𝑖 ) ⊆ 𝑍 ) → ( 𝐹 ↾ ( ℤ𝑖 ) ) Fn ( ℤ𝑖 ) )
104 100 102 103 syl2anc ( ( 𝜑𝑖𝑍 ) → ( 𝐹 ↾ ( ℤ𝑖 ) ) Fn ( ℤ𝑖 ) )
105 104 3adant3 ( ( 𝜑𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) ) → ( 𝐹 ↾ ( ℤ𝑖 ) ) Fn ( ℤ𝑖 ) )
106 simp3 ( ( 𝜑𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) ) → 𝑗 ∈ ( ℤ𝑖 ) )
107 fnfvelrn ( ( ( 𝐹 ↾ ( ℤ𝑖 ) ) Fn ( ℤ𝑖 ) ∧ 𝑗 ∈ ( ℤ𝑖 ) ) → ( ( 𝐹 ↾ ( ℤ𝑖 ) ) ‘ 𝑗 ) ∈ ran ( 𝐹 ↾ ( ℤ𝑖 ) ) )
108 105 106 107 syl2anc ( ( 𝜑𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) ) → ( ( 𝐹 ↾ ( ℤ𝑖 ) ) ‘ 𝑗 ) ∈ ran ( 𝐹 ↾ ( ℤ𝑖 ) ) )
109 98 108 eqeltrd ( ( 𝜑𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) ) → ( 𝐹𝑗 ) ∈ ran ( 𝐹 ↾ ( ℤ𝑖 ) ) )
110 eqid sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < )
111 95 109 110 supxrubd ( ( 𝜑𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) ) → ( 𝐹𝑗 ) ≤ sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) )
112 111 ad5ant134 ( ( ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑖𝑍 ) ∧ 𝑗 ∈ ( ℤ𝑖 ) ) ∧ 𝑥 ≤ ( 𝐹𝑗 ) ) → ( 𝐹𝑗 ) ≤ sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) )
113 86 91 93 94 112 xrletrd ( ( ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑖𝑍 ) ∧ 𝑗 ∈ ( ℤ𝑖 ) ) ∧ 𝑥 ≤ ( 𝐹𝑗 ) ) → 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) )
114 113 rexlimdva2 ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑖𝑍 ) → ( ∃ 𝑗 ∈ ( ℤ𝑖 ) 𝑥 ≤ ( 𝐹𝑗 ) → 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) ) )
115 114 ralimdva ( ( 𝜑𝑥 ∈ ℝ ) → ( ∀ 𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) 𝑥 ≤ ( 𝐹𝑗 ) → ∀ 𝑖𝑍 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) ) )
116 115 reximdva ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) 𝑥 ≤ ( 𝐹𝑗 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑖𝑍 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) ) )
117 84 116 mpd ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑖𝑍 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) )
118 simpl ( ( 𝑦 = 𝑥𝑖𝑍 ) → 𝑦 = 𝑥 )
119 76 adantl ( ( 𝑦 = 𝑥𝑖𝑍 ) → ( ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) ‘ 𝑖 ) = sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) )
120 118 119 breq12d ( ( 𝑦 = 𝑥𝑖𝑍 ) → ( 𝑦 ≤ ( ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) ‘ 𝑖 ) ↔ 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) ) )
121 120 ralbidva ( 𝑦 = 𝑥 → ( ∀ 𝑖𝑍 𝑦 ≤ ( ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) ‘ 𝑖 ) ↔ ∀ 𝑖𝑍 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) ) )
122 121 cbvrexvw ( ∃ 𝑦 ∈ ℝ ∀ 𝑖𝑍 𝑦 ≤ ( ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) ‘ 𝑖 ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑖𝑍 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) )
123 117 122 sylibr ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑖𝑍 𝑦 ≤ ( ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) ‘ 𝑖 ) )
124 2 1 33 79 123 climinf ( 𝜑 → ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) ⇝ inf ( ran ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) , ℝ , < ) )
125 fveq2 ( 𝑛 = 𝑘 → ( ℤ𝑛 ) = ( ℤ𝑘 ) )
126 125 reseq2d ( 𝑛 = 𝑘 → ( 𝐹 ↾ ( ℤ𝑛 ) ) = ( 𝐹 ↾ ( ℤ𝑘 ) ) )
127 126 rneqd ( 𝑛 = 𝑘 → ran ( 𝐹 ↾ ( ℤ𝑛 ) ) = ran ( 𝐹 ↾ ( ℤ𝑘 ) ) )
128 127 supeq1d ( 𝑛 = 𝑘 → sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ𝑘 ) ) , ℝ* , < ) )
129 128 cbvmptv ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) = ( 𝑘𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑘 ) ) , ℝ* , < ) )
130 129 a1i ( 𝜑 → ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) = ( 𝑘𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑘 ) ) , ℝ* , < ) ) )
131 1 2 3 4 limsupvaluz2 ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ran ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) , ℝ , < ) )
132 131 eqcomd ( 𝜑 → inf ( ran ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) , ℝ , < ) = ( lim sup ‘ 𝐹 ) )
133 130 132 breq12d ( 𝜑 → ( ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) ⇝ inf ( ran ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) , ℝ , < ) ↔ ( 𝑘𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑘 ) ) , ℝ* , < ) ) ⇝ ( lim sup ‘ 𝐹 ) ) )
134 124 133 mpbid ( 𝜑 → ( 𝑘𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑘 ) ) , ℝ* , < ) ) ⇝ ( lim sup ‘ 𝐹 ) )