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 ‘ 𝐹 ) )