Metamath Proof Explorer

Theorem o1le

Description: Transfer eventual boundedness from a larger function to a smaller function. (Contributed by Mario Carneiro, 25-Sep-2014) (Proof shortened by Mario Carneiro, 26-May-2016)

Ref Expression
Hypotheses o1le.1 ⊢ φ → M ∈ ℝ
o1le.2 ⊢ φ → x ∈ A ⟼ B ∈ 𝑂⁡1
o1le.3 ⊢ φ ∧ x ∈ A → B ∈ V
o1le.4 ⊢ φ ∧ x ∈ A → C ∈ ℂ
o1le.5 ⊢ φ ∧ x ∈ A ∧ M ≤ x → C ≤ B
Assertion o1le ⊢ φ → x ∈ A ⟼ C ∈ 𝑂⁡1

Proof

Step Hyp Ref Expression
1 o1le.1 ⊢ φ → M ∈ ℝ
2 o1le.2 ⊢ φ → x ∈ A ⟼ B ∈ 𝑂⁡1
3 o1le.3 ⊢ φ ∧ x ∈ A → B ∈ V
4 o1le.4 ⊢ φ ∧ x ∈ A → C ∈ ℂ
5 o1le.5 ⊢ φ ∧ x ∈ A ∧ M ≤ x → C ≤ B
6 3 2 o1mptrcl ⊢ φ ∧ x ∈ A → B ∈ ℂ
7 6 lo1o12 ⊢ φ → x ∈ A ⟼ B ∈ 𝑂⁡1 ↔ x ∈ A ⟼ B ∈ ≤𝑂⁡1
8 2 7 mpbid ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1
9 fvexd ⊢ φ ∧ x ∈ A → B ∈ V
10 4 abscld ⊢ φ ∧ x ∈ A → C ∈ ℝ
11 1 8 9 10 5 lo1le ⊢ φ → x ∈ A ⟼ C ∈ ≤𝑂⁡1
12 4 lo1o12 ⊢ φ → x ∈ A ⟼ C ∈ 𝑂⁡1 ↔ x ∈ A ⟼ C ∈ ≤𝑂⁡1
13 11 12 mpbird ⊢ φ → x ∈ A ⟼ C ∈ 𝑂⁡1