Metamath Proof Explorer


Theorem limsupre2mpt

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 limsupre2mpt.p 𝑥 𝜑
limsupre2mpt.a ( 𝜑𝐴 ⊆ ℝ )
limsupre2mpt.b ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℝ* )
Assertion limsupre2mpt ( 𝜑 → ( ( lim sup ‘ ( 𝑥𝐴𝐵 ) ) ∈ ℝ ↔ ( ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑥𝐴 ( 𝑘𝑥𝑦 < 𝐵 ) ∧ ∃ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑥𝐴 ( 𝑘𝑥𝐵 < 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 limsupre2mpt.p 𝑥 𝜑
2 limsupre2mpt.a ( 𝜑𝐴 ⊆ ℝ )
3 limsupre2mpt.b ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℝ* )
4 nfmpt1 𝑥 ( 𝑥𝐴𝐵 )
5 1 3 fmptd2f ( 𝜑 → ( 𝑥𝐴𝐵 ) : 𝐴 ⟶ ℝ* )
6 4 2 5 limsupre2 ( 𝜑 → ( ( lim sup ‘ ( 𝑥𝐴𝐵 ) ) ∈ ℝ ↔ ( ∃ 𝑤 ∈ ℝ ∀ 𝑗 ∈ ℝ ∃ 𝑥𝐴 ( 𝑗𝑥𝑤 < ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) ) ∧ ∃ 𝑤 ∈ ℝ ∃ 𝑗 ∈ ℝ ∀ 𝑥𝐴 ( 𝑗𝑥 → ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) < 𝑤 ) ) ) )
7 eqid ( 𝑥𝐴𝐵 ) = ( 𝑥𝐴𝐵 )
8 7 a1i ( 𝜑 → ( 𝑥𝐴𝐵 ) = ( 𝑥𝐴𝐵 ) )
9 8 3 fvmpt2d ( ( 𝜑𝑥𝐴 ) → ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) = 𝐵 )
10 9 breq2d ( ( 𝜑𝑥𝐴 ) → ( 𝑤 < ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) ↔ 𝑤 < 𝐵 ) )
11 10 anbi2d ( ( 𝜑𝑥𝐴 ) → ( ( 𝑗𝑥𝑤 < ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) ) ↔ ( 𝑗𝑥𝑤 < 𝐵 ) ) )
12 1 11 rexbida ( 𝜑 → ( ∃ 𝑥𝐴 ( 𝑗𝑥𝑤 < ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) ) ↔ ∃ 𝑥𝐴 ( 𝑗𝑥𝑤 < 𝐵 ) ) )
13 12 ralbidv ( 𝜑 → ( ∀ 𝑗 ∈ ℝ ∃ 𝑥𝐴 ( 𝑗𝑥𝑤 < ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) ) ↔ ∀ 𝑗 ∈ ℝ ∃ 𝑥𝐴 ( 𝑗𝑥𝑤 < 𝐵 ) ) )
14 13 rexbidv ( 𝜑 → ( ∃ 𝑤 ∈ ℝ ∀ 𝑗 ∈ ℝ ∃ 𝑥𝐴 ( 𝑗𝑥𝑤 < ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) ) ↔ ∃ 𝑤 ∈ ℝ ∀ 𝑗 ∈ ℝ ∃ 𝑥𝐴 ( 𝑗𝑥𝑤 < 𝐵 ) ) )
15 9 breq1d ( ( 𝜑𝑥𝐴 ) → ( ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) < 𝑤𝐵 < 𝑤 ) )
16 15 imbi2d ( ( 𝜑𝑥𝐴 ) → ( ( 𝑗𝑥 → ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) < 𝑤 ) ↔ ( 𝑗𝑥𝐵 < 𝑤 ) ) )
17 1 16 ralbida ( 𝜑 → ( ∀ 𝑥𝐴 ( 𝑗𝑥 → ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) < 𝑤 ) ↔ ∀ 𝑥𝐴 ( 𝑗𝑥𝐵 < 𝑤 ) ) )
18 17 rexbidv ( 𝜑 → ( ∃ 𝑗 ∈ ℝ ∀ 𝑥𝐴 ( 𝑗𝑥 → ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) < 𝑤 ) ↔ ∃ 𝑗 ∈ ℝ ∀ 𝑥𝐴 ( 𝑗𝑥𝐵 < 𝑤 ) ) )
19 18 rexbidv ( 𝜑 → ( ∃ 𝑤 ∈ ℝ ∃ 𝑗 ∈ ℝ ∀ 𝑥𝐴 ( 𝑗𝑥 → ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) < 𝑤 ) ↔ ∃ 𝑤 ∈ ℝ ∃ 𝑗 ∈ ℝ ∀ 𝑥𝐴 ( 𝑗𝑥𝐵 < 𝑤 ) ) )
20 14 19 anbi12d ( 𝜑 → ( ( ∃ 𝑤 ∈ ℝ ∀ 𝑗 ∈ ℝ ∃ 𝑥𝐴 ( 𝑗𝑥𝑤 < ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) ) ∧ ∃ 𝑤 ∈ ℝ ∃ 𝑗 ∈ ℝ ∀ 𝑥𝐴 ( 𝑗𝑥 → ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) < 𝑤 ) ) ↔ ( ∃ 𝑤 ∈ ℝ ∀ 𝑗 ∈ ℝ ∃ 𝑥𝐴 ( 𝑗𝑥𝑤 < 𝐵 ) ∧ ∃ 𝑤 ∈ ℝ ∃ 𝑗 ∈ ℝ ∀ 𝑥𝐴 ( 𝑗𝑥𝐵 < 𝑤 ) ) ) )
21 breq1 ( 𝑤 = 𝑦 → ( 𝑤 < 𝐵𝑦 < 𝐵 ) )
22 21 anbi2d ( 𝑤 = 𝑦 → ( ( 𝑗𝑥𝑤 < 𝐵 ) ↔ ( 𝑗𝑥𝑦 < 𝐵 ) ) )
23 22 rexbidv ( 𝑤 = 𝑦 → ( ∃ 𝑥𝐴 ( 𝑗𝑥𝑤 < 𝐵 ) ↔ ∃ 𝑥𝐴 ( 𝑗𝑥𝑦 < 𝐵 ) ) )
24 23 ralbidv ( 𝑤 = 𝑦 → ( ∀ 𝑗 ∈ ℝ ∃ 𝑥𝐴 ( 𝑗𝑥𝑤 < 𝐵 ) ↔ ∀ 𝑗 ∈ ℝ ∃ 𝑥𝐴 ( 𝑗𝑥𝑦 < 𝐵 ) ) )
25 breq1 ( 𝑗 = 𝑘 → ( 𝑗𝑥𝑘𝑥 ) )
26 25 anbi1d ( 𝑗 = 𝑘 → ( ( 𝑗𝑥𝑦 < 𝐵 ) ↔ ( 𝑘𝑥𝑦 < 𝐵 ) ) )
27 26 rexbidv ( 𝑗 = 𝑘 → ( ∃ 𝑥𝐴 ( 𝑗𝑥𝑦 < 𝐵 ) ↔ ∃ 𝑥𝐴 ( 𝑘𝑥𝑦 < 𝐵 ) ) )
28 27 cbvralvw ( ∀ 𝑗 ∈ ℝ ∃ 𝑥𝐴 ( 𝑗𝑥𝑦 < 𝐵 ) ↔ ∀ 𝑘 ∈ ℝ ∃ 𝑥𝐴 ( 𝑘𝑥𝑦 < 𝐵 ) )
29 28 a1i ( 𝑤 = 𝑦 → ( ∀ 𝑗 ∈ ℝ ∃ 𝑥𝐴 ( 𝑗𝑥𝑦 < 𝐵 ) ↔ ∀ 𝑘 ∈ ℝ ∃ 𝑥𝐴 ( 𝑘𝑥𝑦 < 𝐵 ) ) )
30 24 29 bitrd ( 𝑤 = 𝑦 → ( ∀ 𝑗 ∈ ℝ ∃ 𝑥𝐴 ( 𝑗𝑥𝑤 < 𝐵 ) ↔ ∀ 𝑘 ∈ ℝ ∃ 𝑥𝐴 ( 𝑘𝑥𝑦 < 𝐵 ) ) )
31 30 cbvrexvw ( ∃ 𝑤 ∈ ℝ ∀ 𝑗 ∈ ℝ ∃ 𝑥𝐴 ( 𝑗𝑥𝑤 < 𝐵 ) ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑥𝐴 ( 𝑘𝑥𝑦 < 𝐵 ) )
32 breq2 ( 𝑤 = 𝑦 → ( 𝐵 < 𝑤𝐵 < 𝑦 ) )
33 32 imbi2d ( 𝑤 = 𝑦 → ( ( 𝑗𝑥𝐵 < 𝑤 ) ↔ ( 𝑗𝑥𝐵 < 𝑦 ) ) )
34 33 ralbidv ( 𝑤 = 𝑦 → ( ∀ 𝑥𝐴 ( 𝑗𝑥𝐵 < 𝑤 ) ↔ ∀ 𝑥𝐴 ( 𝑗𝑥𝐵 < 𝑦 ) ) )
35 34 rexbidv ( 𝑤 = 𝑦 → ( ∃ 𝑗 ∈ ℝ ∀ 𝑥𝐴 ( 𝑗𝑥𝐵 < 𝑤 ) ↔ ∃ 𝑗 ∈ ℝ ∀ 𝑥𝐴 ( 𝑗𝑥𝐵 < 𝑦 ) ) )
36 25 imbi1d ( 𝑗 = 𝑘 → ( ( 𝑗𝑥𝐵 < 𝑦 ) ↔ ( 𝑘𝑥𝐵 < 𝑦 ) ) )
37 36 ralbidv ( 𝑗 = 𝑘 → ( ∀ 𝑥𝐴 ( 𝑗𝑥𝐵 < 𝑦 ) ↔ ∀ 𝑥𝐴 ( 𝑘𝑥𝐵 < 𝑦 ) ) )
38 37 cbvrexvw ( ∃ 𝑗 ∈ ℝ ∀ 𝑥𝐴 ( 𝑗𝑥𝐵 < 𝑦 ) ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑥𝐴 ( 𝑘𝑥𝐵 < 𝑦 ) )
39 38 a1i ( 𝑤 = 𝑦 → ( ∃ 𝑗 ∈ ℝ ∀ 𝑥𝐴 ( 𝑗𝑥𝐵 < 𝑦 ) ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑥𝐴 ( 𝑘𝑥𝐵 < 𝑦 ) ) )
40 35 39 bitrd ( 𝑤 = 𝑦 → ( ∃ 𝑗 ∈ ℝ ∀ 𝑥𝐴 ( 𝑗𝑥𝐵 < 𝑤 ) ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑥𝐴 ( 𝑘𝑥𝐵 < 𝑦 ) ) )
41 40 cbvrexvw ( ∃ 𝑤 ∈ ℝ ∃ 𝑗 ∈ ℝ ∀ 𝑥𝐴 ( 𝑗𝑥𝐵 < 𝑤 ) ↔ ∃ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑥𝐴 ( 𝑘𝑥𝐵 < 𝑦 ) )
42 31 41 anbi12i ( ( ∃ 𝑤 ∈ ℝ ∀ 𝑗 ∈ ℝ ∃ 𝑥𝐴 ( 𝑗𝑥𝑤 < 𝐵 ) ∧ ∃ 𝑤 ∈ ℝ ∃ 𝑗 ∈ ℝ ∀ 𝑥𝐴 ( 𝑗𝑥𝐵 < 𝑤 ) ) ↔ ( ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑥𝐴 ( 𝑘𝑥𝑦 < 𝐵 ) ∧ ∃ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑥𝐴 ( 𝑘𝑥𝐵 < 𝑦 ) ) )
43 42 a1i ( 𝜑 → ( ( ∃ 𝑤 ∈ ℝ ∀ 𝑗 ∈ ℝ ∃ 𝑥𝐴 ( 𝑗𝑥𝑤 < 𝐵 ) ∧ ∃ 𝑤 ∈ ℝ ∃ 𝑗 ∈ ℝ ∀ 𝑥𝐴 ( 𝑗𝑥𝐵 < 𝑤 ) ) ↔ ( ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑥𝐴 ( 𝑘𝑥𝑦 < 𝐵 ) ∧ ∃ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑥𝐴 ( 𝑘𝑥𝐵 < 𝑦 ) ) ) )
44 6 20 43 3bitrd ( 𝜑 → ( ( lim sup ‘ ( 𝑥𝐴𝐵 ) ) ∈ ℝ ↔ ( ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑥𝐴 ( 𝑘𝑥𝑦 < 𝐵 ) ∧ ∃ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑥𝐴 ( 𝑘𝑥𝐵 < 𝑦 ) ) ) )