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) )