This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lo1const

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

Ref Expression
Assertion lo1const ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 ⊆ ℝ )
2 simplr ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
3 simpr ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ )
4 leid ⊢ ( 𝐵 ∈ ℝ → 𝐵 ≤ 𝐵 )
5 4 ad2antlr ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐵 ≤ 𝑥 ) ) → 𝐵 ≤ 𝐵 )
6 1 2 3 3 5 ello1d ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) )