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 ⊢Ⅎxφ
limsupre3mpt.a ⊢φ→A⊆ℝ
limsupre3mpt.b ⊢φ∧x∈A→B∈ℝ*
Assertion limsupre3mpt ⊢φ→lim sup⁡x∈A⟼B∈ℝ↔∃y∈ℝ∀k∈ℝ∃x∈Ak≤x∧y≤B∧∃y∈ℝ∃k∈ℝ∀x∈Ak≤x→B≤y

Proof

Step Hyp Ref Expression
1 limsupre3mpt.p ⊢Ⅎxφ
2 limsupre3mpt.a ⊢φ→A⊆ℝ
3 limsupre3mpt.b ⊢φ∧x∈A→B∈ℝ*
4 nfmpt1 ⊢Ⅎ_xx∈A⟼B
5 1 3 fmptd2f ⊢φ→x∈A⟼B:A⟶ℝ*
6 4 2 5 limsupre3 ⊢φ→lim sup⁡x∈A⟼B∈ℝ↔∃w∈ℝ∀j∈ℝ∃x∈Aj≤x∧w≤x∈A⟼B⁡x∧∃w∈ℝ∃j∈ℝ∀x∈Aj≤x→x∈A⟼B⁡x≤w
7 eqid ⊢x∈A⟼B=x∈A⟼B
8 7 a1i ⊢φ→x∈A⟼B=x∈A⟼B
9 8 3 fvmpt2d ⊢φ∧x∈A→x∈A⟼B⁡x=B
10 9 breq2d ⊢φ∧x∈A→w≤x∈A⟼B⁡x↔w≤B
11 10 anbi2d ⊢φ∧x∈A→j≤x∧w≤x∈A⟼B⁡x↔j≤x∧w≤B
12 1 11 rexbida ⊢φ→∃x∈Aj≤x∧w≤x∈A⟼B⁡x↔∃x∈Aj≤x∧w≤B
13 12 ralbidv ⊢φ→∀j∈ℝ∃x∈Aj≤x∧w≤x∈A⟼B⁡x↔∀j∈ℝ∃x∈Aj≤x∧w≤B
14 13 rexbidv ⊢φ→∃w∈ℝ∀j∈ℝ∃x∈Aj≤x∧w≤x∈A⟼B⁡x↔∃w∈ℝ∀j∈ℝ∃x∈Aj≤x∧w≤B
15 9 breq1d ⊢φ∧x∈A→x∈A⟼B⁡x≤w↔B≤w
16 15 imbi2d ⊢φ∧x∈A→j≤x→x∈A⟼B⁡x≤w↔j≤x→B≤w
17 1 16 ralbida ⊢φ→∀x∈Aj≤x→x∈A⟼B⁡x≤w↔∀x∈Aj≤x→B≤w
18 17 rexbidv ⊢φ→∃j∈ℝ∀x∈Aj≤x→x∈A⟼B⁡x≤w↔∃j∈ℝ∀x∈Aj≤x→B≤w
19 18 rexbidv ⊢φ→∃w∈ℝ∃j∈ℝ∀x∈Aj≤x→x∈A⟼B⁡x≤w↔∃w∈ℝ∃j∈ℝ∀x∈Aj≤x→B≤w
20 14 19 anbi12d ⊢φ→∃w∈ℝ∀j∈ℝ∃x∈Aj≤x∧w≤x∈A⟼B⁡x∧∃w∈ℝ∃j∈ℝ∀x∈Aj≤x→x∈A⟼B⁡x≤w↔∃w∈ℝ∀j∈ℝ∃x∈Aj≤x∧w≤B∧∃w∈ℝ∃j∈ℝ∀x∈Aj≤x→B≤w
21 breq1 ⊢w=y→w≤B↔y≤B
22 21 anbi2d ⊢w=y→j≤x∧w≤B↔j≤x∧y≤B
23 22 rexbidv ⊢w=y→∃x∈Aj≤x∧w≤B↔∃x∈Aj≤x∧y≤B
24 23 ralbidv ⊢w=y→∀j∈ℝ∃x∈Aj≤x∧w≤B↔∀j∈ℝ∃x∈Aj≤x∧y≤B
25 breq1 ⊢j=k→j≤x↔k≤x
26 25 anbi1d ⊢j=k→j≤x∧y≤B↔k≤x∧y≤B
27 26 rexbidv ⊢j=k→∃x∈Aj≤x∧y≤B↔∃x∈Ak≤x∧y≤B
28 27 cbvralvw ⊢∀j∈ℝ∃x∈Aj≤x∧y≤B↔∀k∈ℝ∃x∈Ak≤x∧y≤B
29 28 a1i ⊢w=y→∀j∈ℝ∃x∈Aj≤x∧y≤B↔∀k∈ℝ∃x∈Ak≤x∧y≤B
30 24 29 bitrd ⊢w=y→∀j∈ℝ∃x∈Aj≤x∧w≤B↔∀k∈ℝ∃x∈Ak≤x∧y≤B
31 30 cbvrexvw ⊢∃w∈ℝ∀j∈ℝ∃x∈Aj≤x∧w≤B↔∃y∈ℝ∀k∈ℝ∃x∈Ak≤x∧y≤B
32 breq2 ⊢w=y→B≤w↔B≤y
33 32 imbi2d ⊢w=y→j≤x→B≤w↔j≤x→B≤y
34 33 ralbidv ⊢w=y→∀x∈Aj≤x→B≤w↔∀x∈Aj≤x→B≤y
35 34 rexbidv ⊢w=y→∃j∈ℝ∀x∈Aj≤x→B≤w↔∃j∈ℝ∀x∈Aj≤x→B≤y
36 25 imbi1d ⊢j=k→j≤x→B≤y↔k≤x→B≤y
37 36 ralbidv ⊢j=k→∀x∈Aj≤x→B≤y↔∀x∈Ak≤x→B≤y
38 37 cbvrexvw ⊢∃j∈ℝ∀x∈Aj≤x→B≤y↔∃k∈ℝ∀x∈Ak≤x→B≤y
39 38 a1i ⊢w=y→∃j∈ℝ∀x∈Aj≤x→B≤y↔∃k∈ℝ∀x∈Ak≤x→B≤y
40 35 39 bitrd ⊢w=y→∃j∈ℝ∀x∈Aj≤x→B≤w↔∃k∈ℝ∀x∈Ak≤x→B≤y
41 40 cbvrexvw ⊢∃w∈ℝ∃j∈ℝ∀x∈Aj≤x→B≤w↔∃y∈ℝ∃k∈ℝ∀x∈Ak≤x→B≤y
42 31 41 anbi12i ⊢∃w∈ℝ∀j∈ℝ∃x∈Aj≤x∧w≤B∧∃w∈ℝ∃j∈ℝ∀x∈Aj≤x→B≤w↔∃y∈ℝ∀k∈ℝ∃x∈Ak≤x∧y≤B∧∃y∈ℝ∃k∈ℝ∀x∈Ak≤x→B≤y
43 42 a1i ⊢φ→∃w∈ℝ∀j∈ℝ∃x∈Aj≤x∧w≤B∧∃w∈ℝ∃j∈ℝ∀x∈Aj≤x→B≤w↔∃y∈ℝ∀k∈ℝ∃x∈Ak≤x∧y≤B∧∃y∈ℝ∃k∈ℝ∀x∈Ak≤x→B≤y
44 6 20 43 3bitrd ⊢φ→lim sup⁡x∈A⟼B∈ℝ↔∃y∈ℝ∀k∈ℝ∃x∈Ak≤x∧y≤B∧∃y∈ℝ∃k∈ℝ∀x∈Ak≤x→B≤y