Theorem o1bdd2

Description: If an eventually bounded function is bounded on every interval A i^i ( -oo , y ) by a function M ( y ) , then the function is bounded on the whole domain. (Contributed by Mario Carneiro, 9-Apr-2016) (Proof shortened by Mario Carneiro, 26-May-2016)

	Ref	Expression
Hypotheses	o1bdd2.1	$$⊢\phi \to A\subseteq ℝ$$
	o1bdd2.2	$$⊢\phi \to C\in ℝ$$
	o1bdd2.3	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℂ$$
	o1bdd2.4	$$⊢\phi \to \left(x\in A⟼B\right)\in 𝑂\left(1\right)$$
	o1bdd2.5	$$⊢\left(\phi \wedge \left(y\in ℝ\wedge C\le y\right)\right)\to M\in ℝ$$
	o1bdd2.6	$$⊢\left(\left(\phi \wedge x\in A\right)\wedge \left(\left(y\in ℝ\wedge C\le y\right)\wedge x<y\right)\right)\to \left|B\right|\le M$$
Assertion	o1bdd2	$$⊢\phi \to \exists m\in ℝ\forall x\in A\left|B\right|\le m$$

Proof

Step	Hyp	Ref	Expression
1		o1bdd2.1	$$⊢\phi \to A\subseteq ℝ$$
2		o1bdd2.2	$$⊢\phi \to C\in ℝ$$
3		o1bdd2.3	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℂ$$
4		o1bdd2.4	$$⊢\phi \to \left(x\in A⟼B\right)\in 𝑂\left(1\right)$$
5		o1bdd2.5	$$⊢\left(\phi \wedge \left(y\in ℝ\wedge C\le y\right)\right)\to M\in ℝ$$
6		o1bdd2.6	$$⊢\left(\left(\phi \wedge x\in A\right)\wedge \left(\left(y\in ℝ\wedge C\le y\right)\wedge x<y\right)\right)\to \left|B\right|\le M$$
7	3	abscld	$$⊢\left(\phi \wedge x\in A\right)\to \left|B\right|\in ℝ$$
8	3	lo1o12	$$⊢\phi \to \left(\left(x\in A⟼B\right)\in 𝑂\left(1\right)\leftrightarrow \left(x\in A⟼\left|B\right|\right)\in \le 𝑂\left(1\right)\right)$$
9	4 8	mpbid	$$⊢\phi \to \left(x\in A⟼\left|B\right|\right)\in \le 𝑂\left(1\right)$$
10	1 2 7 9 5 6	lo1bdd2	$$⊢\phi \to \exists m\in ℝ\forall x\in A\left|B\right|\le m$$