Metamath Proof Explorer

Theorem o1bdd2

Description: If an eventually bounded function is bounded on every interval A i^i ( -oo , y ) by a function M ( y ) , then the function is bounded on the whole domain. (Contributed by Mario Carneiro, 9-Apr-2016) (Proof shortened by Mario Carneiro, 26-May-2016)

Ref Expression
Hypotheses o1bdd2.1 ⊢ φ → A ⊆ ℝ
o1bdd2.2 ⊢ φ → C ∈ ℝ
o1bdd2.3 ⊢ φ ∧ x ∈ A → B ∈ ℂ
o1bdd2.4 ⊢ φ → x ∈ A ⟼ B ∈ 𝑂⁡1
o1bdd2.5 ⊢ φ ∧ y ∈ ℝ ∧ C ≤ y → M ∈ ℝ
o1bdd2.6 ⊢ φ ∧ x ∈ A ∧ y ∈ ℝ ∧ C ≤ y ∧ x < y → B ≤ M
Assertion o1bdd2 ⊢ φ → ∃ m ∈ ℝ ∀ x ∈ A B ≤ m

Proof

Step Hyp Ref Expression
1 o1bdd2.1 ⊢ φ → A ⊆ ℝ
2 o1bdd2.2 ⊢ φ → C ∈ ℝ
3 o1bdd2.3 ⊢ φ ∧ x ∈ A → B ∈ ℂ
4 o1bdd2.4 ⊢ φ → x ∈ A ⟼ B ∈ 𝑂⁡1
5 o1bdd2.5 ⊢ φ ∧ y ∈ ℝ ∧ C ≤ y → M ∈ ℝ
6 o1bdd2.6 ⊢ φ ∧ x ∈ A ∧ y ∈ ℝ ∧ C ≤ y ∧ x < y → B ≤ M
7 3 abscld ⊢ φ ∧ x ∈ A → B ∈ ℝ
8 3 lo1o12 ⊢ φ → x ∈ A ⟼ B ∈ 𝑂⁡1 ↔ x ∈ A ⟼ B ∈ ≤𝑂⁡1
9 4 8 mpbid ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1
10 1 2 7 9 5 6 lo1bdd2 ⊢ φ → ∃ m ∈ ℝ ∀ x ∈ A B ≤ m