Theorem o1lo1d

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

	Ref	Expression
Hypotheses	o1lo1.1	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
	lo1o1.1	$$⊢\phi \to \left(x\in A⟼B\right)\in 𝑂\left(1\right)$$
Assertion	o1lo1d	$$⊢\phi \to \left(x\in A⟼B\right)\in \le 𝑂\left(1\right)$$

Proof

Step	Hyp	Ref	Expression
1		o1lo1.1	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
2		lo1o1.1	$$⊢\phi \to \left(x\in A⟼B\right)\in 𝑂\left(1\right)$$
3	1	o1lo1	$$⊢\phi \to \left(\left(x\in A⟼B\right)\in 𝑂\left(1\right)\leftrightarrow \left(\left(x\in A⟼B\right)\in \le 𝑂\left(1\right)\wedge \left(x\in A⟼-B\right)\in \le 𝑂\left(1\right)\right)\right)$$
4	2 3	mpbid	$$⊢\phi \to \left(\left(x\in A⟼B\right)\in \le 𝑂\left(1\right)\wedge \left(x\in A⟼-B\right)\in \le 𝑂\left(1\right)\right)$$
5	4	simpld	$$⊢\phi \to \left(x\in A⟼B\right)\in \le 𝑂\left(1\right)$$