Metamath Proof Explorer

Theorem limsupre3mpt

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

Proof

Step Hyp Ref Expression
1 limsupre3mpt.p ⊢ Ⅎ 𝑥 𝜑
2 limsupre3mpt.a ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
3 limsupre3mpt.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
4 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
5 1 3 fmptd2f ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℝ* )
6 4 2 5 limsupre3 ⊢ ( 𝜑 → ( ( 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 ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ↔ ( ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑥 ∈ 𝐴 ( 𝑘 ≤ 𝑥 ∧ 𝑦 ≤ 𝐵 ) ∧ ∃ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑘 ≤ 𝑥 → 𝐵 ≤ 𝑦 ) ) ) )