Theorem o1lo1d

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

	Ref	Expression
Hypotheses	o1lo1.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
	lo1o1.1	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) )
Assertion	o1lo1d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) )

Proof

Step	Hyp	Ref	Expression
1		o1lo1.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
2		lo1o1.1	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) )
3	1	o1lo1	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ∧ ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ∈ ≤𝑂(1) ) ) )
4	2 3	mpbid	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ∧ ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ∈ ≤𝑂(1) ) )
5	4	simpld	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) )