# Metamath Proof Explorer

## Theorem ello1mpt2

Description: Elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Hypotheses ello1mpt.1 ${⊢}{\phi }\to {A}\subseteq ℝ$
ello1mpt.2 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in ℝ$
ello1d.3 ${⊢}{\phi }\to {C}\in ℝ$
Assertion ello1mpt2 ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right)\in \le 𝑂\left(1\right)↔\exists {y}\in \left[{C},\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {m}\right)\right)$

### Proof

Step Hyp Ref Expression
1 ello1mpt.1 ${⊢}{\phi }\to {A}\subseteq ℝ$
2 ello1mpt.2 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in ℝ$
3 ello1d.3 ${⊢}{\phi }\to {C}\in ℝ$
4 1 2 ello1mpt ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right)\in \le 𝑂\left(1\right)↔\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {m}\right)\right)$
5 rexico ${⊢}\left({A}\subseteq ℝ\wedge {C}\in ℝ\right)\to \left(\exists {y}\in \left[{C},\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {m}\right)↔\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {m}\right)\right)$
6 1 3 5 syl2anc ${⊢}{\phi }\to \left(\exists {y}\in \left[{C},\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {m}\right)↔\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {m}\right)\right)$
7 6 rexbidv ${⊢}{\phi }\to \left(\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in \left[{C},\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {m}\right)↔\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {m}\right)\right)$
8 rexcom ${⊢}\exists {y}\in \left[{C},\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {m}\right)↔\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in \left[{C},\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {m}\right)$
9 rexcom ${⊢}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {m}\right)↔\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {m}\right)$
10 7 8 9 3bitr4g ${⊢}{\phi }\to \left(\exists {y}\in \left[{C},\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {m}\right)↔\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {m}\right)\right)$
11 4 10 bitr4d ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right)\in \le 𝑂\left(1\right)↔\exists {y}\in \left[{C},\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {m}\right)\right)$