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 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( 𝐹 ‘ 𝑚 ) ∈ ℝ )
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 40 41 syl ⊢ ( 𝑖 ∈ 𝑍 → ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ⊆ ( ℤ≥ ‘ 𝑖 ) )
43 ssres2 ⊢ ( ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ⊆ ( ℤ≥ ‘ 𝑖 ) → ( 𝐹 ↾ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ) ⊆ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) )
44 42 43 syl ⊢ ( 𝑖 ∈ 𝑍 → ( 𝐹 ↾ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ) ⊆ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) )
45 rnss ⊢ ( ( 𝐹 ↾ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ) ⊆ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) → ran ( 𝐹 ↾ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ) ⊆ ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) )
46 44 45 syl ⊢ ( 𝑖 ∈ 𝑍 → ran ( 𝐹 ↾ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ) ⊆ ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) )
47 46 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ran ( 𝐹 ↾ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ) ⊆ ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) )
48 rnresss ⊢ ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) ⊆ ran 𝐹
49 48 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) ⊆ ran 𝐹 )
50 3 frnd ⊢ ( 𝜑 → ran 𝐹 ⊆ ℝ )
51 50 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ran 𝐹 ⊆ ℝ )
52 49 51 sstrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) ⊆ ℝ )
53 ressxr ⊢ ℝ ⊆ ℝ*
54 53 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ℝ ⊆ ℝ* )
55 52 54 sstrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) ⊆ ℝ* )
56 supxrss ⊢ ( ( ran ( 𝐹 ↾ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ) ⊆ ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) ∧ ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) ⊆ ℝ* ) → sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ) , ℝ* , < ) ≤ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) )
57 47 55 56 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ) , ℝ* , < ) ≤ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) )
58 eqidd ⊢ ( 𝑖 ∈ 𝑍 → ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) = ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) )
59 fveq2 ⊢ ( 𝑛 = ( 𝑖 + 1 ) → ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ ( 𝑖 + 1 ) ) )
60 59 reseq2d ⊢ ( 𝑛 = ( 𝑖 + 1 ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) = ( 𝐹 ↾ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ) )
61 60 rneqd ⊢ ( 𝑛 = ( 𝑖 + 1 ) → ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) = ran ( 𝐹 ↾ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ) )
62 61 supeq1d ⊢ ( 𝑛 = ( 𝑖 + 1 ) → sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ) , ℝ* , < ) )
63 62 adantl ⊢ ( ( 𝑖 ∈ 𝑍 ∧ 𝑛 = ( 𝑖 + 1 ) ) → sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ) , ℝ* , < ) )
64 2 peano2uzs ⊢ ( 𝑖 ∈ 𝑍 → ( 𝑖 + 1 ) ∈ 𝑍 )
65 xrltso ⊢ < Or ℝ*
66 65 supex ⊢ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ) , ℝ* , < ) ∈ V
67 66 a1i ⊢ ( 𝑖 ∈ 𝑍 → sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ) , ℝ* , < ) ∈ V )
68 58 63 64 67 fvmptd ⊢ ( 𝑖 ∈ 𝑍 → ( ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) ‘ ( 𝑖 + 1 ) ) = sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ) , ℝ* , < ) )
69 68 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) ‘ ( 𝑖 + 1 ) ) = sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ) , ℝ* , < ) )
70 fveq2 ⊢ ( 𝑛 = 𝑖 → ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ 𝑖 ) )
71 70 reseq2d ⊢ ( 𝑛 = 𝑖 → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) = ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) )
72 71 rneqd ⊢ ( 𝑛 = 𝑖 → ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) = ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) )
73 72 supeq1d ⊢ ( 𝑛 = 𝑖 → sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) )
74 73 adantl ⊢ ( ( 𝑖 ∈ 𝑍 ∧ 𝑛 = 𝑖 ) → sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) )
75 id ⊢ ( 𝑖 ∈ 𝑍 → 𝑖 ∈ 𝑍 )
76 65 supex ⊢ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) ∈ V
77 76 a1i ⊢ ( 𝑖 ∈ 𝑍 → sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) ∈ V )
78 58 74 75 77 fvmptd ⊢ ( 𝑖 ∈ 𝑍 → ( ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) ‘ 𝑖 ) = sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) )
79 78 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) ‘ 𝑖 ) = sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) )
80 69 79 breq12d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( ( ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) ‘ ( 𝑖 + 1 ) ) ≤ ( ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) ‘ 𝑖 ) ↔ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ) , ℝ* , < ) ≤ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) ) )
81 57 80 mpbird ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) ‘ ( 𝑖 + 1 ) ) ≤ ( ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) ‘ 𝑖 ) )
82 nfcv ⊢ Ⅎ 𝑗 𝐹
83 3 frexr ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
84 82 1 2 83 limsupre3uz ⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
85 4 84 mpbid ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
86 85 simpld ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
87 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → 𝑥 ∈ ℝ )
88 87 rexrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → 𝑥 ∈ ℝ* )
89 83 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝐹 : 𝑍 ⟶ ℝ* )
90 2 uztrn2 ⊢ ( ( 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑗 ∈ 𝑍 )
91 90 3adant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑗 ∈ 𝑍 )
92 89 91 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
93 92 ad5ant134 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
94 55 supxrcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) ∈ ℝ* )
95 94 ad5ant13 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) ∈ ℝ* )
96 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
97 55 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) ⊆ ℝ* )
98 fvres ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) ‘ 𝑗 ) = ( 𝐹 ‘ 𝑗 ) )
99 98 eqcomd ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) → ( 𝐹 ‘ 𝑗 ) = ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) ‘ 𝑗 ) )
100 99 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( 𝐹 ‘ 𝑗 ) = ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) ‘ 𝑗 ) )
101 3 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝑍 )
102 101 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → 𝐹 Fn 𝑍 )
103 2 75 uzssd2 ⊢ ( 𝑖 ∈ 𝑍 → ( ℤ≥ ‘ 𝑖 ) ⊆ 𝑍 )
104 103 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( ℤ≥ ‘ 𝑖 ) ⊆ 𝑍 )
105 fnssres ⊢ ( ( 𝐹 Fn 𝑍 ∧ ( ℤ≥ ‘ 𝑖 ) ⊆ 𝑍 ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) Fn ( ℤ≥ ‘ 𝑖 ) )
106 102 104 105 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) Fn ( ℤ≥ ‘ 𝑖 ) )
107 106 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) Fn ( ℤ≥ ‘ 𝑖 ) )
108 simp3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) )
109 fnfvelrn ⊢ ( ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) Fn ( ℤ≥ ‘ 𝑖 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) ‘ 𝑗 ) ∈ ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) )
110 107 108 109 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) ‘ 𝑗 ) ∈ ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) )
111 100 110 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) )
112 eqid ⊢ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < )
113 97 111 112 supxrubd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( 𝐹 ‘ 𝑗 ) ≤ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) )
114 113 ad5ant134 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑗 ) ≤ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) )
115 88 93 95 96 114 xrletrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) )
116 115 rexlimdva2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ 𝑍 ) → ( ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) → 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) ) )
117 116 ralimdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑖 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) → ∀ 𝑖 ∈ 𝑍 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) ) )
118 117 reximdva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝑍 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) ) )
119 86 118 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝑍 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) )
120 simpl ⊢ ( ( 𝑦 = 𝑥 ∧ 𝑖 ∈ 𝑍 ) → 𝑦 = 𝑥 )
121 78 adantl ⊢ ( ( 𝑦 = 𝑥 ∧ 𝑖 ∈ 𝑍 ) → ( ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) ‘ 𝑖 ) = sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) )
122 120 121 breq12d ⊢ ( ( 𝑦 = 𝑥 ∧ 𝑖 ∈ 𝑍 ) → ( 𝑦 ≤ ( ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) ‘ 𝑖 ) ↔ 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) ) )
123 122 ralbidva ⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑖 ∈ 𝑍 𝑦 ≤ ( ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) ‘ 𝑖 ) ↔ ∀ 𝑖 ∈ 𝑍 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) ) )
124 123 cbvrexvw ⊢ ( ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ 𝑍 𝑦 ≤ ( ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) ‘ 𝑖 ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝑍 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) )
125 119 124 sylibr ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ 𝑍 𝑦 ≤ ( ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) ‘ 𝑖 ) )
126 2 1 33 81 125 climinf ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) ⇝ inf ( ran ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) , ℝ , < ) )
127 fveq2 ⊢ ( 𝑛 = 𝑘 → ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ 𝑘 ) )
128 127 reseq2d ⊢ ( 𝑛 = 𝑘 → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) = ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) )
129 128 rneqd ⊢ ( 𝑛 = 𝑘 → ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) = ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) )
130 129 supeq1d ⊢ ( 𝑛 = 𝑘 → sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) )
131 130 cbvmptv ⊢ ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) = ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) )
132 131 a1i ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) = ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) ) )
133 1 2 3 4 limsupvaluz2 ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ran ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) , ℝ , < ) )
134 133 eqcomd ⊢ ( 𝜑 → inf ( ran ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) , ℝ , < ) = ( lim sup ‘ 𝐹 ) )
135 132 134 breq12d ⊢ ( 𝜑 → ( ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) ⇝ inf ( ran ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) , ℝ , < ) ↔ ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) ) ⇝ ( lim sup ‘ 𝐹 ) ) )
136 126 135 mpbid ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) ) ⇝ ( lim sup ‘ 𝐹 ) )