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 ∈ A k ≤ x ∧ y ≤ B ∧ ∃ y ∈ ℝ ∃ k ∈ ℝ ∀ x ∈ A k ≤ x → B ≤ y

Proof

Step Hyp Ref Expression
1 limsupre3mpt.p ⊢ Ⅎ x φ
2 limsupre3mpt.a ⊢ φ → A ⊆ ℝ
3 limsupre3mpt.b ⊢ φ ∧ x ∈ A → B ∈ ℝ *
4 nfmpt1 ⊢ Ⅎ _ x x ∈ A ⟼ B
5 1 3 fmptd2f ⊢ φ → x ∈ A ⟼ B : A ⟶ ℝ *
6 4 2 5 limsupre3 ⊢ φ → lim sup ⁡ x ∈ A ⟼ B ∈ ℝ ↔ ∃ w ∈ ℝ ∀ j ∈ ℝ ∃ x ∈ A j ≤ x ∧ w ≤ x ∈ A ⟼ B ⁡ x ∧ ∃ w ∈ ℝ ∃ j ∈ ℝ ∀ x ∈ A j ≤ 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 ∈ A j ≤ x ∧ w ≤ x ∈ A ⟼ B ⁡ x ↔ ∃ x ∈ A j ≤ x ∧ w ≤ B
13 12 ralbidv ⊢ φ → ∀ j ∈ ℝ ∃ x ∈ A j ≤ x ∧ w ≤ x ∈ A ⟼ B ⁡ x ↔ ∀ j ∈ ℝ ∃ x ∈ A j ≤ x ∧ w ≤ B
14 13 rexbidv ⊢ φ → ∃ w ∈ ℝ ∀ j ∈ ℝ ∃ x ∈ A j ≤ x ∧ w ≤ x ∈ A ⟼ B ⁡ x ↔ ∃ w ∈ ℝ ∀ j ∈ ℝ ∃ x ∈ A j ≤ 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 ∈ A j ≤ x → x ∈ A ⟼ B ⁡ x ≤ w ↔ ∀ x ∈ A j ≤ x → B ≤ w
18 17 rexbidv ⊢ φ → ∃ j ∈ ℝ ∀ x ∈ A j ≤ x → x ∈ A ⟼ B ⁡ x ≤ w ↔ ∃ j ∈ ℝ ∀ x ∈ A j ≤ x → B ≤ w
19 18 rexbidv ⊢ φ → ∃ w ∈ ℝ ∃ j ∈ ℝ ∀ x ∈ A j ≤ x → x ∈ A ⟼ B ⁡ x ≤ w ↔ ∃ w ∈ ℝ ∃ j ∈ ℝ ∀ x ∈ A j ≤ x → B ≤ w
20 14 19 anbi12d ⊢ φ → ∃ w ∈ ℝ ∀ j ∈ ℝ ∃ x ∈ A j ≤ x ∧ w ≤ x ∈ A ⟼ B ⁡ x ∧ ∃ w ∈ ℝ ∃ j ∈ ℝ ∀ x ∈ A j ≤ x → x ∈ A ⟼ B ⁡ x ≤ w ↔ ∃ w ∈ ℝ ∀ j ∈ ℝ ∃ x ∈ A j ≤ x ∧ w ≤ B ∧ ∃ w ∈ ℝ ∃ j ∈ ℝ ∀ x ∈ A j ≤ 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 ∈ A j ≤ x ∧ w ≤ B ↔ ∃ x ∈ A j ≤ x ∧ y ≤ B
24 23 ralbidv ⊢ w = y → ∀ j ∈ ℝ ∃ x ∈ A j ≤ x ∧ w ≤ B ↔ ∀ j ∈ ℝ ∃ x ∈ A j ≤ 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 ∈ A j ≤ x ∧ y ≤ B ↔ ∃ x ∈ A k ≤ x ∧ y ≤ B
28 27 cbvralvw ⊢ ∀ j ∈ ℝ ∃ x ∈ A j ≤ x ∧ y ≤ B ↔ ∀ k ∈ ℝ ∃ x ∈ A k ≤ x ∧ y ≤ B
29 28 a1i ⊢ w = y → ∀ j ∈ ℝ ∃ x ∈ A j ≤ x ∧ y ≤ B ↔ ∀ k ∈ ℝ ∃ x ∈ A k ≤ x ∧ y ≤ B
30 24 29 bitrd ⊢ w = y → ∀ j ∈ ℝ ∃ x ∈ A j ≤ x ∧ w ≤ B ↔ ∀ k ∈ ℝ ∃ x ∈ A k ≤ x ∧ y ≤ B
31 30 cbvrexvw ⊢ ∃ w ∈ ℝ ∀ j ∈ ℝ ∃ x ∈ A j ≤ x ∧ w ≤ B ↔ ∃ y ∈ ℝ ∀ k ∈ ℝ ∃ x ∈ A k ≤ 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 ∈ A j ≤ x → B ≤ w ↔ ∀ x ∈ A j ≤ x → B ≤ y
35 34 rexbidv ⊢ w = y → ∃ j ∈ ℝ ∀ x ∈ A j ≤ x → B ≤ w ↔ ∃ j ∈ ℝ ∀ x ∈ A j ≤ x → B ≤ y
36 25 imbi1d ⊢ j = k → j ≤ x → B ≤ y ↔ k ≤ x → B ≤ y
37 36 ralbidv ⊢ j = k → ∀ x ∈ A j ≤ x → B ≤ y ↔ ∀ x ∈ A k ≤ x → B ≤ y
38 37 cbvrexvw ⊢ ∃ j ∈ ℝ ∀ x ∈ A j ≤ x → B ≤ y ↔ ∃ k ∈ ℝ ∀ x ∈ A k ≤ x → B ≤ y
39 38 a1i ⊢ w = y → ∃ j ∈ ℝ ∀ x ∈ A j ≤ x → B ≤ y ↔ ∃ k ∈ ℝ ∀ x ∈ A k ≤ x → B ≤ y
40 35 39 bitrd ⊢ w = y → ∃ j ∈ ℝ ∀ x ∈ A j ≤ x → B ≤ w ↔ ∃ k ∈ ℝ ∀ x ∈ A k ≤ x → B ≤ y
41 40 cbvrexvw ⊢ ∃ w ∈ ℝ ∃ j ∈ ℝ ∀ x ∈ A j ≤ x → B ≤ w ↔ ∃ y ∈ ℝ ∃ k ∈ ℝ ∀ x ∈ A k ≤ x → B ≤ y
42 31 41 anbi12i ⊢ ∃ w ∈ ℝ ∀ j ∈ ℝ ∃ x ∈ A j ≤ x ∧ w ≤ B ∧ ∃ w ∈ ℝ ∃ j ∈ ℝ ∀ x ∈ A j ≤ x → B ≤ w ↔ ∃ y ∈ ℝ ∀ k ∈ ℝ ∃ x ∈ A k ≤ x ∧ y ≤ B ∧ ∃ y ∈ ℝ ∃ k ∈ ℝ ∀ x ∈ A k ≤ x → B ≤ y
43 42 a1i ⊢ φ → ∃ w ∈ ℝ ∀ j ∈ ℝ ∃ x ∈ A j ≤ x ∧ w ≤ B ∧ ∃ w ∈ ℝ ∃ j ∈ ℝ ∀ x ∈ A j ≤ x → B ≤ w ↔ ∃ y ∈ ℝ ∀ k ∈ ℝ ∃ x ∈ A k ≤ x ∧ y ≤ B ∧ ∃ y ∈ ℝ ∃ k ∈ ℝ ∀ x ∈ A k ≤ x → B ≤ y
44 6 20 43 3bitrd ⊢ φ → lim sup ⁡ x ∈ A ⟼ B ∈ ℝ ↔ ∃ y ∈ ℝ ∀ k ∈ ℝ ∃ x ∈ A k ≤ x ∧ y ≤ B ∧ ∃ y ∈ ℝ ∃ k ∈ ℝ ∀ x ∈ A k ≤ x → B ≤ y