Metamath Proof Explorer

Theorem limsupre2

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 smaller than the function, at some point, in any upper part of the reals; 2. there is a real number that is eventually larger than the function. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 limsupre2.1 ⊢ Ⅎ 𝑗 𝐹
2 limsupre2.2 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
3 limsupre2.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
4 nfcv ⊢ Ⅎ 𝑙 𝐹
5 4 2 3 limsupre2lem ⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ ℝ ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑦 < ( 𝐹 ‘ 𝑙 ) ) ∧ ∃ 𝑦 ∈ ℝ ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) < 𝑦 ) ) ) )
6 breq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 < ( 𝐹 ‘ 𝑙 ) ↔ 𝑥 < ( 𝐹 ‘ 𝑙 ) ) )
7 6 anbi2d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑖 ≤ 𝑙 ∧ 𝑦 < ( 𝐹 ‘ 𝑙 ) ) ↔ ( 𝑖 ≤ 𝑙 ∧ 𝑥 < ( 𝐹 ‘ 𝑙 ) ) ) )
8 7 rexbidv ⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑦 < ( 𝐹 ‘ 𝑙 ) ) ↔ ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑥 < ( 𝐹 ‘ 𝑙 ) ) ) )
9 8 ralbidv ⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑖 ∈ ℝ ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑦 < ( 𝐹 ‘ 𝑙 ) ) ↔ ∀ 𝑖 ∈ ℝ ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑥 < ( 𝐹 ‘ 𝑙 ) ) ) )
10 breq1 ⊢ ( 𝑖 = 𝑘 → ( 𝑖 ≤ 𝑙 ↔ 𝑘 ≤ 𝑙 ) )
11 10 anbi1d ⊢ ( 𝑖 = 𝑘 → ( ( 𝑖 ≤ 𝑙 ∧ 𝑥 < ( 𝐹 ‘ 𝑙 ) ) ↔ ( 𝑘 ≤ 𝑙 ∧ 𝑥 < ( 𝐹 ‘ 𝑙 ) ) ) )
12 11 rexbidv ⊢ ( 𝑖 = 𝑘 → ( ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑥 < ( 𝐹 ‘ 𝑙 ) ) ↔ ∃ 𝑙 ∈ 𝐴 ( 𝑘 ≤ 𝑙 ∧ 𝑥 < ( 𝐹 ‘ 𝑙 ) ) ) )
13 nfv ⊢ Ⅎ 𝑗 𝑘 ≤ 𝑙
14 nfcv ⊢ Ⅎ 𝑗 𝑥
15 nfcv ⊢ Ⅎ 𝑗 <
16 nfcv ⊢ Ⅎ 𝑗 𝑙
17 1 16 nffv ⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 )
18 14 15 17 nfbr ⊢ Ⅎ 𝑗 𝑥 < ( 𝐹 ‘ 𝑙 )
19 13 18 nfan ⊢ Ⅎ 𝑗 ( 𝑘 ≤ 𝑙 ∧ 𝑥 < ( 𝐹 ‘ 𝑙 ) )
20 nfv ⊢ Ⅎ 𝑙 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) )
21 breq2 ⊢ ( 𝑙 = 𝑗 → ( 𝑘 ≤ 𝑙 ↔ 𝑘 ≤ 𝑗 ) )
22 fveq2 ⊢ ( 𝑙 = 𝑗 → ( 𝐹 ‘ 𝑙 ) = ( 𝐹 ‘ 𝑗 ) )
23 22 breq2d ⊢ ( 𝑙 = 𝑗 → ( 𝑥 < ( 𝐹 ‘ 𝑙 ) ↔ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) )
24 21 23 anbi12d ⊢ ( 𝑙 = 𝑗 → ( ( 𝑘 ≤ 𝑙 ∧ 𝑥 < ( 𝐹 ‘ 𝑙 ) ) ↔ ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) )
25 19 20 24 cbvrexw ⊢ ( ∃ 𝑙 ∈ 𝐴 ( 𝑘 ≤ 𝑙 ∧ 𝑥 < ( 𝐹 ‘ 𝑙 ) ) ↔ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) )
26 25 a1i ⊢ ( 𝑖 = 𝑘 → ( ∃ 𝑙 ∈ 𝐴 ( 𝑘 ≤ 𝑙 ∧ 𝑥 < ( 𝐹 ‘ 𝑙 ) ) ↔ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) )
27 12 26 bitrd ⊢ ( 𝑖 = 𝑘 → ( ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑥 < ( 𝐹 ‘ 𝑙 ) ) ↔ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) )
28 27 cbvralvw ⊢ ( ∀ 𝑖 ∈ ℝ ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑥 < ( 𝐹 ‘ 𝑙 ) ) ↔ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) )
29 28 a1i ⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑖 ∈ ℝ ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑥 < ( 𝐹 ‘ 𝑙 ) ) ↔ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) )
30 9 29 bitrd ⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑖 ∈ ℝ ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑦 < ( 𝐹 ‘ 𝑙 ) ) ↔ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) )
31 30 cbvrexvw ⊢ ( ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ ℝ ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑦 < ( 𝐹 ‘ 𝑙 ) ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) )
32 31 a1i ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ ℝ ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑦 < ( 𝐹 ‘ 𝑙 ) ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) )
33 breq2 ⊢ ( 𝑦 = 𝑥 → ( ( 𝐹 ‘ 𝑙 ) < 𝑦 ↔ ( 𝐹 ‘ 𝑙 ) < 𝑥 ) )
34 33 imbi2d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) < 𝑦 ) ↔ ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) < 𝑥 ) ) )
35 34 ralbidv ⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) < 𝑦 ) ↔ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) < 𝑥 ) ) )
36 35 rexbidv ⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) < 𝑦 ) ↔ ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) < 𝑥 ) ) )
37 10 imbi1d ⊢ ( 𝑖 = 𝑘 → ( ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) < 𝑥 ) ↔ ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) < 𝑥 ) ) )
38 37 ralbidv ⊢ ( 𝑖 = 𝑘 → ( ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) < 𝑥 ) ↔ ∀ 𝑙 ∈ 𝐴 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) < 𝑥 ) ) )
39 17 15 14 nfbr ⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 ) < 𝑥
40 13 39 nfim ⊢ Ⅎ 𝑗 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) < 𝑥 )
41 nfv ⊢ Ⅎ 𝑙 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑥 )
42 22 breq1d ⊢ ( 𝑙 = 𝑗 → ( ( 𝐹 ‘ 𝑙 ) < 𝑥 ↔ ( 𝐹 ‘ 𝑗 ) < 𝑥 ) )
43 21 42 imbi12d ⊢ ( 𝑙 = 𝑗 → ( ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) < 𝑥 ) ↔ ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑥 ) ) )
44 40 41 43 cbvralw ⊢ ( ∀ 𝑙 ∈ 𝐴 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) < 𝑥 ) ↔ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑥 ) )
45 44 a1i ⊢ ( 𝑖 = 𝑘 → ( ∀ 𝑙 ∈ 𝐴 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) < 𝑥 ) ↔ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑥 ) ) )
46 38 45 bitrd ⊢ ( 𝑖 = 𝑘 → ( ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) < 𝑥 ) ↔ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑥 ) ) )
47 46 cbvrexvw ⊢ ( ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) < 𝑥 ) ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑥 ) )
48 47 a1i ⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) < 𝑥 ) ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑥 ) ) )
49 36 48 bitrd ⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) < 𝑦 ) ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑥 ) ) )
50 49 cbvrexvw ⊢ ( ∃ 𝑦 ∈ ℝ ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) < 𝑦 ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑥 ) )
51 50 a1i ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) < 𝑦 ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑥 ) ) )
52 32 51 anbi12d ⊢ ( 𝜑 → ( ( ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ ℝ ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑦 < ( 𝐹 ‘ 𝑙 ) ) ∧ ∃ 𝑦 ∈ ℝ ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) < 𝑦 ) ) ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑥 ) ) ) )
53 5 52 bitrd ⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < 𝑥 ) ) ) )