Metamath Proof Explorer

Theorem lo1const

Description: A constant function is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Assertion lo1const ⊢ A ⊆ ℝ ∧ B ∈ ℝ → x ∈ A ⟼ B ∈ ≤𝑂⁡1

Proof

Step Hyp Ref Expression
1 simpl ⊢ A ⊆ ℝ ∧ B ∈ ℝ → A ⊆ ℝ
2 simplr ⊢ A ⊆ ℝ ∧ B ∈ ℝ ∧ x ∈ A → B ∈ ℝ
3 simpr ⊢ A ⊆ ℝ ∧ B ∈ ℝ → B ∈ ℝ
4 leid ⊢ B ∈ ℝ → B ≤ B
5 4 ad2antlr ⊢ A ⊆ ℝ ∧ B ∈ ℝ ∧ x ∈ A ∧ B ≤ x → B ≤ B
6 1 2 3 3 5 ello1d ⊢ A ⊆ ℝ ∧ B ∈ ℝ → x ∈ A ⟼ B ∈ ≤𝑂⁡1