Metamath Proof Explorer

Theorem limsupvaluz2

Description: The superior limit, when the domain of a real-valued function is a set of upper integers, and the superior limit is real. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsupvaluz2.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
limsupvaluz2.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
limsupvaluz2.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
limsupvaluz2.r ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ∈ ℝ )
Assertion limsupvaluz2 ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ran ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) ) , ℝ , < ) )

Proof

Step Hyp Ref Expression
1 limsupvaluz2.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2 limsupvaluz2.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 limsupvaluz2.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
4 limsupvaluz2.r ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ∈ ℝ )
5 3 frexr ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
6 1 2 5 limsupvaluz ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ran ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) , ℝ* , < ) )
7 3 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝐹 : 𝑍 ⟶ ℝ )
8 id ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ 𝑍 )
9 2 8 uzssd2 ⊢ ( 𝑛 ∈ 𝑍 → ( ℤ≥ ‘ 𝑛 ) ⊆ 𝑍 )
10 9 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ℤ≥ ‘ 𝑛 ) ⊆ 𝑍 )
11 7 10 feqresmpt ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) = ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( 𝐹 ‘ 𝑚 ) ) )
12 11 rneqd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) = ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( 𝐹 ‘ 𝑚 ) ) )
13 12 supeq1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) = sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( 𝐹 ‘ 𝑚 ) ) , ℝ* , < ) )
14 nfcv ⊢ Ⅎ 𝑚 𝐹
15 4 renepnfd ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ≠ +∞ )
16 14 2 3 15 limsupubuz ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑚 ∈ 𝑍 ( 𝐹 ‘ 𝑚 ) ≤ 𝑥 )
17 16 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑚 ∈ 𝑍 ( 𝐹 ‘ 𝑚 ) ≤ 𝑥 )
18 ssralv ⊢ ( ( ℤ≥ ‘ 𝑛 ) ⊆ 𝑍 → ( ∀ 𝑚 ∈ 𝑍 ( 𝐹 ‘ 𝑚 ) ≤ 𝑥 → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑥 ) )
19 9 18 syl ⊢ ( 𝑛 ∈ 𝑍 → ( ∀ 𝑚 ∈ 𝑍 ( 𝐹 ‘ 𝑚 ) ≤ 𝑥 → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑥 ) )
20 19 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ∀ 𝑚 ∈ 𝑍 ( 𝐹 ‘ 𝑚 ) ≤ 𝑥 → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑥 ) )
21 20 reximdv ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑚 ∈ 𝑍 ( 𝐹 ‘ 𝑚 ) ≤ 𝑥 → ∃ 𝑥 ∈ ℝ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑥 ) )
22 17 21 mpd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑥 )
23 nfv ⊢ Ⅎ 𝑚 ( 𝜑 ∧ 𝑛 ∈ 𝑍 )
24 2 eluzelz2 ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ )
25 uzid ⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ( ℤ≥ ‘ 𝑛 ) )
26 ne0i ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑛 ) → ( ℤ≥ ‘ 𝑛 ) ≠ ∅ )
27 24 25 26 3syl ⊢ ( 𝑛 ∈ 𝑍 → ( ℤ≥ ‘ 𝑛 ) ≠ ∅ )
28 27 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ℤ≥ ‘ 𝑛 ) ≠ ∅ )
29 7 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝐹 : 𝑍 ⟶ ℝ )
30 10 sselda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ 𝑍 )
31 29 30 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( 𝐹 ‘ 𝑚 ) ∈ ℝ )
32 23 28 31 supxrre3rnmpt ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( 𝐹 ‘ 𝑚 ) ) , ℝ* , < ) ∈ ℝ ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑥 ) )
33 22 32 mpbird ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → sup ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ↦ ( 𝐹 ‘ 𝑚 ) ) , ℝ* , < ) ∈ ℝ )
34 13 33 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ∈ ℝ )
35 34 fmpttd ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) : 𝑍 ⟶ ℝ )
36 35 frnd ⊢ ( 𝜑 → ran ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) ⊆ ℝ )
37 nfv ⊢ Ⅎ 𝑛 𝜑
38 eqid ⊢ ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) = ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) )
39 1 2 uzn0d ⊢ ( 𝜑 → 𝑍 ≠ ∅ )
40 37 34 38 39 rnmptn0 ⊢ ( 𝜑 → ran ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) ≠ ∅ )
41 nfcv ⊢ Ⅎ 𝑗 𝐹
42 41 1 2 5 limsupre3uz ⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
43 4 42 mpbid ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
44 43 simpld ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
45 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → 𝑥 ∈ ℝ )
46 45 rexrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → 𝑥 ∈ ℝ* )
47 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝐹 : 𝑍 ⟶ ℝ* )
48 2 uztrn2 ⊢ ( ( 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑗 ∈ 𝑍 )
49 48 3adant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑗 ∈ 𝑍 )
50 47 49 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
51 50 ad5ant134 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
52 rnresss ⊢ ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) ⊆ ran 𝐹
53 52 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) ⊆ ran 𝐹 )
54 3 frnd ⊢ ( 𝜑 → ran 𝐹 ⊆ ℝ )
55 54 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ran 𝐹 ⊆ ℝ )
56 53 55 sstrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) ⊆ ℝ )
57 ressxr ⊢ ℝ ⊆ ℝ*
58 57 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ℝ ⊆ ℝ* )
59 56 58 sstrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) ⊆ ℝ* )
60 59 supxrcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) ∈ ℝ* )
61 60 ad5ant13 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) ∈ ℝ* )
62 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
63 59 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) ⊆ ℝ* )
64 fvres ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) ‘ 𝑗 ) = ( 𝐹 ‘ 𝑗 ) )
65 64 eqcomd ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) → ( 𝐹 ‘ 𝑗 ) = ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) ‘ 𝑗 ) )
66 65 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( 𝐹 ‘ 𝑗 ) = ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) ‘ 𝑗 ) )
67 3 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝑍 )
68 67 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → 𝐹 Fn 𝑍 )
69 id ⊢ ( 𝑖 ∈ 𝑍 → 𝑖 ∈ 𝑍 )
70 2 69 uzssd2 ⊢ ( 𝑖 ∈ 𝑍 → ( ℤ≥ ‘ 𝑖 ) ⊆ 𝑍 )
71 70 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( ℤ≥ ‘ 𝑖 ) ⊆ 𝑍 )
72 fnssres ⊢ ( ( 𝐹 Fn 𝑍 ∧ ( ℤ≥ ‘ 𝑖 ) ⊆ 𝑍 ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) Fn ( ℤ≥ ‘ 𝑖 ) )
73 68 71 72 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) Fn ( ℤ≥ ‘ 𝑖 ) )
74 73 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) Fn ( ℤ≥ ‘ 𝑖 ) )
75 simp3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) )
76 fnfvelrn ⊢ ( ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) Fn ( ℤ≥ ‘ 𝑖 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) ‘ 𝑗 ) ∈ ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) )
77 74 75 76 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) ‘ 𝑗 ) ∈ ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) )
78 66 77 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) )
79 eqid ⊢ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < )
80 63 78 79 supxrubd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( 𝐹 ‘ 𝑗 ) ≤ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) )
81 80 ad5ant134 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑗 ) ≤ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) )
82 46 51 61 62 81 xrletrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) )
83 82 rexlimdva2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ 𝑍 ) → ( ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) → 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) ) )
84 83 ralimdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑖 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) → ∀ 𝑖 ∈ 𝑍 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) ) )
85 84 reximdva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝑍 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) ) )
86 44 85 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝑍 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) )
87 86 idi ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝑍 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) )
88 fveq2 ⊢ ( 𝑛 = 𝑖 → ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ 𝑖 ) )
89 88 reseq2d ⊢ ( 𝑛 = 𝑖 → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) = ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) )
90 89 rneqd ⊢ ( 𝑛 = 𝑖 → ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) = ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) )
91 90 supeq1d ⊢ ( 𝑛 = 𝑖 → sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) )
92 eqcom ⊢ ( 𝑛 = 𝑖 ↔ 𝑖 = 𝑛 )
93 92 imbi1i ⊢ ( ( 𝑛 = 𝑖 → sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) ) ↔ ( 𝑖 = 𝑛 → sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) ) )
94 eqcom ⊢ ( sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) ↔ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) )
95 94 imbi2i ⊢ ( ( 𝑖 = 𝑛 → sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) ) ↔ ( 𝑖 = 𝑛 → sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) )
96 93 95 bitri ⊢ ( ( 𝑛 = 𝑖 → sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) ) ↔ ( 𝑖 = 𝑛 → sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) )
97 91 96 mpbi ⊢ ( 𝑖 = 𝑛 → sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) )
98 97 breq2d ⊢ ( 𝑖 = 𝑛 → ( 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) ↔ 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) )
99 98 cbvralvw ⊢ ( ∀ 𝑖 ∈ 𝑍 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) ↔ ∀ 𝑛 ∈ 𝑍 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) )
100 99 rexbii ⊢ ( ∃ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝑍 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑖 ) ) , ℝ* , < ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) )
101 87 100 sylib ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) )
102 34 elexd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ∈ V )
103 37 102 rnmptbd2 ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) 𝑥 ≤ 𝑦 ) )
104 101 103 mpbid ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) 𝑥 ≤ 𝑦 )
105 infxrre ⊢ ( ( ran ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) ⊆ ℝ ∧ ran ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) 𝑥 ≤ 𝑦 ) → inf ( ran ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) , ℝ* , < ) = inf ( ran ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) , ℝ , < ) )
106 36 40 104 105 syl3anc ⊢ ( 𝜑 → inf ( ran ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) , ℝ* , < ) = inf ( ran ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) , ℝ , < ) )
107 fveq2 ⊢ ( 𝑛 = 𝑘 → ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ 𝑘 ) )
108 107 reseq2d ⊢ ( 𝑛 = 𝑘 → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) = ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) )
109 108 rneqd ⊢ ( 𝑛 = 𝑘 → ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) = ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) )
110 109 supeq1d ⊢ ( 𝑛 = 𝑘 → sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) )
111 110 cbvmptv ⊢ ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) = ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) )
112 111 rneqi ⊢ ran ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) = ran ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) )
113 112 infeq1i ⊢ inf ( ran ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) , ℝ , < ) = inf ( ran ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) ) , ℝ , < )
114 113 a1i ⊢ ( 𝜑 → inf ( ran ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) , ℝ , < ) = inf ( ran ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) ) , ℝ , < ) )
115 6 106 114 3eqtrd ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ran ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) ) , ℝ , < ) )