# Metamath Proof Explorer

## Theorem elo1d

Description: Sufficient condition for elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 21-Sep-2014) (Proof shortened by Mario Carneiro, 26-May-2016)

Ref Expression
Hypotheses elo1mpt.1 ${⊢}{\phi }\to {A}\subseteq ℝ$
elo1mpt.2 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in ℂ$
elo1d.3 ${⊢}{\phi }\to {C}\in ℝ$
elo1d.4 ${⊢}{\phi }\to {M}\in ℝ$
elo1d.5 ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {C}\le {x}\right)\right)\to \left|{B}\right|\le {M}$
Assertion elo1d ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right)\in 𝑂\left(1\right)$

### Proof

Step Hyp Ref Expression
1 elo1mpt.1 ${⊢}{\phi }\to {A}\subseteq ℝ$
2 elo1mpt.2 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in ℂ$
3 elo1d.3 ${⊢}{\phi }\to {C}\in ℝ$
4 elo1d.4 ${⊢}{\phi }\to {M}\in ℝ$
5 elo1d.5 ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {C}\le {x}\right)\right)\to \left|{B}\right|\le {M}$
6 2 abscld ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left|{B}\right|\in ℝ$
7 1 6 3 4 5 ello1d ${⊢}{\phi }\to \left({x}\in {A}⟼\left|{B}\right|\right)\in \le 𝑂\left(1\right)$
8 2 lo1o12 ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right)\in 𝑂\left(1\right)↔\left({x}\in {A}⟼\left|{B}\right|\right)\in \le 𝑂\left(1\right)\right)$
9 7 8 mpbird ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right)\in 𝑂\left(1\right)$