Metamath Proof Explorer

Theorem limsupre3lem

Description: Given a function on the extended reals, its supremum limit is real if and only if two condition holds: 1. there is a real number that is less than or equal to the function, at some point, in any upper part of the reals; 2. there is a real number that is eventually greater than or equal to the function. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsupre3lem.1 ⊢ Ⅎ 𝑗 𝐹
limsupre3lem.2 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
limsupre3lem.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
Assertion limsupre3lem ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 limsupre3lem.1 ⊢ Ⅎ 𝑗 𝐹
2 limsupre3lem.2 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
3 limsupre3lem.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
4 1 2 3 limsupre2 ⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑦 < ( 𝐹 ‘ 𝑗 ) ) ∧ ∃ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑦 ) ) ) )
5 simp2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑦 < ( 𝐹 ‘ 𝑗 ) ) ) → 𝑦 ∈ ℝ )
6 nfv ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑦 ∈ ℝ )
7 simp3l ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ∧ ( 𝑘 ≤ 𝑗 ∧ 𝑦 < ( 𝐹 ‘ 𝑗 ) ) ) → 𝑘 ≤ 𝑗 )
8 simp1r ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ∧ 𝑦 < ( 𝐹 ‘ 𝑗 ) ) → 𝑦 ∈ ℝ )
9 8 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ∧ 𝑦 < ( 𝐹 ‘ 𝑗 ) ) → 𝑦 ∈ ℝ* )
10 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
11 10 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
12 11 3adant3 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ∧ 𝑦 < ( 𝐹 ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
13 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ∧ 𝑦 < ( 𝐹 ‘ 𝑗 ) ) → 𝑦 < ( 𝐹 ‘ 𝑗 ) )
14 9 12 13 xrltled ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ∧ 𝑦 < ( 𝐹 ‘ 𝑗 ) ) → 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) )
15 14 3adant3l ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ∧ ( 𝑘 ≤ 𝑗 ∧ 𝑦 < ( 𝐹 ‘ 𝑗 ) ) ) → 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) )
16 7 15 jca ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ∧ ( 𝑘 ≤ 𝑗 ∧ 𝑦 < ( 𝐹 ‘ 𝑗 ) ) ) → ( 𝑘 ≤ 𝑗 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) )
17 16 3exp ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑗 ∈ 𝐴 → ( ( 𝑘 ≤ 𝑗 ∧ 𝑦 < ( 𝐹 ‘ 𝑗 ) ) → ( 𝑘 ≤ 𝑗 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ) ) )
18 6 17 reximdai ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑦 < ( 𝐹 ‘ 𝑗 ) ) → ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
19 18 ralimdv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑦 < ( 𝐹 ‘ 𝑗 ) ) → ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
20 19 3impia ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑦 < ( 𝐹 ‘ 𝑗 ) ) ) → ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) )
21 breq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ↔ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) )
22 21 anbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ( 𝑘 ≤ 𝑗 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
23 22 rexbidv ⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
24 23 ralbidv ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
25 24 rspcev ⊢ ( ( 𝑦 ∈ ℝ ∧ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
26 5 20 25 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑦 < ( 𝐹 ‘ 𝑗 ) ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
27 26 3exp ⊢ ( 𝜑 → ( 𝑦 ∈ ℝ → ( ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑦 < ( 𝐹 ‘ 𝑗 ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) ) )
28 27 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑦 < ( 𝐹 ‘ 𝑗 ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
29 peano2rem ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 − 1 ) ∈ ℝ )
30 29 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) → ( 𝑥 − 1 ) ∈ ℝ )
31 nfv ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑥 ∈ ℝ )
32 simp3l ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ∧ ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) → 𝑘 ≤ 𝑗 )
33 simp1r ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ∧ ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) → 𝑥 ∈ ℝ )
34 29 rexrd ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 − 1 ) ∈ ℝ* )
35 33 34 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ∧ ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) → ( 𝑥 − 1 ) ∈ ℝ* )
36 33 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ∧ ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) → 𝑥 ∈ ℝ* )
37 10 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
38 37 3adant3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ∧ ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
39 33 ltm1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ∧ ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) → ( 𝑥 − 1 ) < 𝑥 )
40 simp3r ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ∧ ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) → 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
41 35 36 38 39 40 xrltletrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ∧ ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) → ( 𝑥 − 1 ) < ( 𝐹 ‘ 𝑗 ) )
42 32 41 jca ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ∧ ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) → ( 𝑘 ≤ 𝑗 ∧ ( 𝑥 − 1 ) < ( 𝐹 ‘ 𝑗 ) ) )
43 42 3exp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑗 ∈ 𝐴 → ( ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ( 𝑘 ≤ 𝑗 ∧ ( 𝑥 − 1 ) < ( 𝐹 ‘ 𝑗 ) ) ) ) )
44 31 43 reximdai ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ ( 𝑥 − 1 ) < ( 𝐹 ‘ 𝑗 ) ) ) )
45 44 ralimdv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ ( 𝑥 − 1 ) < ( 𝐹 ‘ 𝑗 ) ) ) )
46 45 imp ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) → ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ ( 𝑥 − 1 ) < ( 𝐹 ‘ 𝑗 ) ) )
47 breq1 ⊢ ( 𝑦 = ( 𝑥 − 1 ) → ( 𝑦 < ( 𝐹 ‘ 𝑗 ) ↔ ( 𝑥 − 1 ) < ( 𝐹 ‘ 𝑗 ) ) )
48 47 anbi2d ⊢ ( 𝑦 = ( 𝑥 − 1 ) → ( ( 𝑘 ≤ 𝑗 ∧ 𝑦 < ( 𝐹 ‘ 𝑗 ) ) ↔ ( 𝑘 ≤ 𝑗 ∧ ( 𝑥 − 1 ) < ( 𝐹 ‘ 𝑗 ) ) ) )
49 48 rexbidv ⊢ ( 𝑦 = ( 𝑥 − 1 ) → ( ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑦 < ( 𝐹 ‘ 𝑗 ) ) ↔ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ ( 𝑥 − 1 ) < ( 𝐹 ‘ 𝑗 ) ) ) )
50 49 ralbidv ⊢ ( 𝑦 = ( 𝑥 − 1 ) → ( ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑦 < ( 𝐹 ‘ 𝑗 ) ) ↔ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ ( 𝑥 − 1 ) < ( 𝐹 ‘ 𝑗 ) ) ) )
51 50 rspcev ⊢ ( ( ( 𝑥 − 1 ) ∈ ℝ ∧ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ ( 𝑥 − 1 ) < ( 𝐹 ‘ 𝑗 ) ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑦 < ( 𝐹 ‘ 𝑗 ) ) )
52 30 46 51 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑦 < ( 𝐹 ‘ 𝑗 ) ) )
53 52 rexlimdva2 ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑦 < ( 𝐹 ‘ 𝑗 ) ) ) )
54 28 53 impbid ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑦 < ( 𝐹 ‘ 𝑗 ) ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
55 simplr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑦 ) ) → 𝑦 ∈ ℝ )
56 11 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑗 ) < 𝑦 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
57 rexr ⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℝ* )
58 57 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑗 ) < 𝑦 ) → 𝑦 ∈ ℝ* )
59 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑗 ) < 𝑦 ) → ( 𝐹 ‘ 𝑗 ) < 𝑦 )
60 56 58 59 xrltled ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑗 ) < 𝑦 ) → ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 )
61 60 ex ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑗 ) < 𝑦 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 ) )
62 61 imim2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑦 ) → ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 ) ) )
63 62 ralimdva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑦 ) → ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 ) ) )
64 63 reximdv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑦 ) → ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 ) ) )
65 64 imp ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑦 ) ) → ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 ) )
66 breq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 ) )
67 66 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 ) ) )
68 67 ralbidv ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 ) ) )
69 68 rexbidv ⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 ) ) )
70 69 rspcev ⊢ ( ( 𝑦 ∈ ℝ ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 ) ) → ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
71 55 65 70 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑦 ) ) → ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
72 71 rexlimdva2 ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑦 ) → ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
73 peano2re ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 + 1 ) ∈ ℝ )
74 73 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) → ( 𝑥 + 1 ) ∈ ℝ )
75 37 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
76 rexr ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
77 76 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → 𝑥 ∈ ℝ* )
78 73 rexrd ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 + 1 ) ∈ ℝ* )
79 78 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ( 𝑥 + 1 ) ∈ ℝ* )
80 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
81 ltp1 ⊢ ( 𝑥 ∈ ℝ → 𝑥 < ( 𝑥 + 1 ) )
82 81 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → 𝑥 < ( 𝑥 + 1 ) )
83 75 77 79 80 82 xrlelttrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ( 𝐹 ‘ 𝑗 ) < ( 𝑥 + 1 ) )
84 83 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 → ( 𝐹 ‘ 𝑗 ) < ( 𝑥 + 1 ) ) )
85 84 imim2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < ( 𝑥 + 1 ) ) ) )
86 85 ralimdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < ( 𝑥 + 1 ) ) ) )
87 86 reximdv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < ( 𝑥 + 1 ) ) ) )
88 87 imp ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) → ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < ( 𝑥 + 1 ) ) )
89 breq2 ⊢ ( 𝑦 = ( 𝑥 + 1 ) → ( ( 𝐹 ‘ 𝑗 ) < 𝑦 ↔ ( 𝐹 ‘ 𝑗 ) < ( 𝑥 + 1 ) ) )
90 89 imbi2d ⊢ ( 𝑦 = ( 𝑥 + 1 ) → ( ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑦 ) ↔ ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < ( 𝑥 + 1 ) ) ) )
91 90 ralbidv ⊢ ( 𝑦 = ( 𝑥 + 1 ) → ( ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑦 ) ↔ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < ( 𝑥 + 1 ) ) ) )
92 91 rexbidv ⊢ ( 𝑦 = ( 𝑥 + 1 ) → ( ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑦 ) ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < ( 𝑥 + 1 ) ) ) )
93 92 rspcev ⊢ ( ( ( 𝑥 + 1 ) ∈ ℝ ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < ( 𝑥 + 1 ) ) ) → ∃ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑦 ) )
94 74 88 93 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) → ∃ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑦 ) )
95 94 rexlimdva2 ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ∃ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑦 ) ) )
96 72 95 impbid ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑦 ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
97 54 96 anbi12d ⊢ ( 𝜑 → ( ( ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑦 < ( 𝐹 ‘ 𝑗 ) ) ∧ ∃ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑦 ) ) ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ) )
98 4 97 bitrd ⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ) )