# Metamath Proof Explorer

## Theorem ello1mpt

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 ℝ$
Assertion 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)$

### 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 2 fmpttd ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right):{A}⟶ℝ$
4 ello12 ${⊢}\left(\left({x}\in {A}⟼{B}\right):{A}⟶ℝ\wedge {A}\subseteq ℝ\right)\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 {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left({x}\in {A}⟼{B}\right)\left({z}\right)\le {m}\right)\right)$
5 3 1 4 syl2anc ${⊢}{\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 {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left({x}\in {A}⟼{B}\right)\left({z}\right)\le {m}\right)\right)$
6 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}\le {z}$
7 nffvmpt1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}⟼{B}\right)\left({z}\right)$
8 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\le$
9 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{m}$
10 7 8 9 nfbr ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}⟼{B}\right)\left({z}\right)\le {m}$
11 6 10 nfim ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left({x}\in {A}⟼{B}\right)\left({z}\right)\le {m}\right)$
12 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to \left({x}\in {A}⟼{B}\right)\left({x}\right)\le {m}\right)$
13 breq2 ${⊢}{z}={x}\to \left({y}\le {z}↔{y}\le {x}\right)$
14 fveq2 ${⊢}{z}={x}\to \left({x}\in {A}⟼{B}\right)\left({z}\right)=\left({x}\in {A}⟼{B}\right)\left({x}\right)$
15 14 breq1d ${⊢}{z}={x}\to \left(\left({x}\in {A}⟼{B}\right)\left({z}\right)\le {m}↔\left({x}\in {A}⟼{B}\right)\left({x}\right)\le {m}\right)$
16 13 15 imbi12d ${⊢}{z}={x}\to \left(\left({y}\le {z}\to \left({x}\in {A}⟼{B}\right)\left({z}\right)\le {m}\right)↔\left({y}\le {x}\to \left({x}\in {A}⟼{B}\right)\left({x}\right)\le {m}\right)\right)$
17 11 12 16 cbvralw ${⊢}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left({x}\in {A}⟼{B}\right)\left({z}\right)\le {m}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to \left({x}\in {A}⟼{B}\right)\left({x}\right)\le {m}\right)$
18 simpr ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {x}\in {A}$
19 eqid ${⊢}\left({x}\in {A}⟼{B}\right)=\left({x}\in {A}⟼{B}\right)$
20 19 fvmpt2 ${⊢}\left({x}\in {A}\wedge {B}\in ℝ\right)\to \left({x}\in {A}⟼{B}\right)\left({x}\right)={B}$
21 18 2 20 syl2anc ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({x}\in {A}⟼{B}\right)\left({x}\right)={B}$
22 21 breq1d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left(\left({x}\in {A}⟼{B}\right)\left({x}\right)\le {m}↔{B}\le {m}\right)$
23 22 imbi2d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left(\left({y}\le {x}\to \left({x}\in {A}⟼{B}\right)\left({x}\right)\le {m}\right)↔\left({y}\le {x}\to {B}\le {m}\right)\right)$
24 23 ralbidva ${⊢}{\phi }\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to \left({x}\in {A}⟼{B}\right)\left({x}\right)\le {m}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {m}\right)\right)$
25 17 24 syl5bb ${⊢}{\phi }\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left({x}\in {A}⟼{B}\right)\left({z}\right)\le {m}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {m}\right)\right)$
26 25 2rexbidv ${⊢}{\phi }\to \left(\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {z}\to \left({x}\in {A}⟼{B}\right)\left({z}\right)\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)$
27 5 26 bitrd ${⊢}{\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)$