# Metamath Proof Explorer

## Theorem elbigo

Description: Properties of a function of order G(x). (Contributed by AV, 16-May-2020)

Ref Expression
Assertion elbigo ${⊢}{F}\in O\left({G}\right)↔\left({F}\in \left(ℝ{↑}_{𝑝𝑚}ℝ\right)\wedge {G}\in \left(ℝ{↑}_{𝑝𝑚}ℝ\right)\wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left(\mathrm{dom}{F}\cap \left[{x},\mathrm{+\infty }\right)\right)\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {m}{G}\left({y}\right)\right)$

### Proof

Step Hyp Ref Expression
1 bigoval ${⊢}{G}\in \left(ℝ{↑}_{𝑝𝑚}ℝ\right)\to O\left({G}\right)=\left\{{f}\in \left(ℝ{↑}_{𝑝𝑚}ℝ\right)|\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left(\mathrm{dom}{f}\cap \left[{x},\mathrm{+\infty }\right)\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\le {m}{G}\left({y}\right)\right\}$
2 1 eleq2d ${⊢}{G}\in \left(ℝ{↑}_{𝑝𝑚}ℝ\right)\to \left({F}\in O\left({G}\right)↔{F}\in \left\{{f}\in \left(ℝ{↑}_{𝑝𝑚}ℝ\right)|\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left(\mathrm{dom}{f}\cap \left[{x},\mathrm{+\infty }\right)\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\le {m}{G}\left({y}\right)\right\}\right)$
3 dmeq ${⊢}{f}={F}\to \mathrm{dom}{f}=\mathrm{dom}{F}$
4 3 ineq1d ${⊢}{f}={F}\to \mathrm{dom}{f}\cap \left[{x},\mathrm{+\infty }\right)=\mathrm{dom}{F}\cap \left[{x},\mathrm{+\infty }\right)$
5 fveq1 ${⊢}{f}={F}\to {f}\left({y}\right)={F}\left({y}\right)$
6 5 breq1d ${⊢}{f}={F}\to \left({f}\left({y}\right)\le {m}{G}\left({y}\right)↔{F}\left({y}\right)\le {m}{G}\left({y}\right)\right)$
7 4 6 raleqbidv ${⊢}{f}={F}\to \left(\forall {y}\in \left(\mathrm{dom}{f}\cap \left[{x},\mathrm{+\infty }\right)\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\le {m}{G}\left({y}\right)↔\forall {y}\in \left(\mathrm{dom}{F}\cap \left[{x},\mathrm{+\infty }\right)\right)\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {m}{G}\left({y}\right)\right)$
8 7 2rexbidv ${⊢}{f}={F}\to \left(\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left(\mathrm{dom}{f}\cap \left[{x},\mathrm{+\infty }\right)\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\le {m}{G}\left({y}\right)↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left(\mathrm{dom}{F}\cap \left[{x},\mathrm{+\infty }\right)\right)\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {m}{G}\left({y}\right)\right)$
9 8 elrab ${⊢}{F}\in \left\{{f}\in \left(ℝ{↑}_{𝑝𝑚}ℝ\right)|\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left(\mathrm{dom}{f}\cap \left[{x},\mathrm{+\infty }\right)\right)\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\le {m}{G}\left({y}\right)\right\}↔\left({F}\in \left(ℝ{↑}_{𝑝𝑚}ℝ\right)\wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left(\mathrm{dom}{F}\cap \left[{x},\mathrm{+\infty }\right)\right)\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {m}{G}\left({y}\right)\right)$
10 2 9 syl6bb ${⊢}{G}\in \left(ℝ{↑}_{𝑝𝑚}ℝ\right)\to \left({F}\in O\left({G}\right)↔\left({F}\in \left(ℝ{↑}_{𝑝𝑚}ℝ\right)\wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left(\mathrm{dom}{F}\cap \left[{x},\mathrm{+\infty }\right)\right)\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {m}{G}\left({y}\right)\right)\right)$
11 10 pm5.32i ${⊢}\left({G}\in \left(ℝ{↑}_{𝑝𝑚}ℝ\right)\wedge {F}\in O\left({G}\right)\right)↔\left({G}\in \left(ℝ{↑}_{𝑝𝑚}ℝ\right)\wedge \left({F}\in \left(ℝ{↑}_{𝑝𝑚}ℝ\right)\wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left(\mathrm{dom}{F}\cap \left[{x},\mathrm{+\infty }\right)\right)\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {m}{G}\left({y}\right)\right)\right)$
12 elbigofrcl ${⊢}{F}\in O\left({G}\right)\to {G}\in \left(ℝ{↑}_{𝑝𝑚}ℝ\right)$
13 12 pm4.71ri ${⊢}{F}\in O\left({G}\right)↔\left({G}\in \left(ℝ{↑}_{𝑝𝑚}ℝ\right)\wedge {F}\in O\left({G}\right)\right)$
14 3anan12 ${⊢}\left({F}\in \left(ℝ{↑}_{𝑝𝑚}ℝ\right)\wedge {G}\in \left(ℝ{↑}_{𝑝𝑚}ℝ\right)\wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left(\mathrm{dom}{F}\cap \left[{x},\mathrm{+\infty }\right)\right)\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {m}{G}\left({y}\right)\right)↔\left({G}\in \left(ℝ{↑}_{𝑝𝑚}ℝ\right)\wedge \left({F}\in \left(ℝ{↑}_{𝑝𝑚}ℝ\right)\wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left(\mathrm{dom}{F}\cap \left[{x},\mathrm{+\infty }\right)\right)\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {m}{G}\left({y}\right)\right)\right)$
15 11 13 14 3bitr4i ${⊢}{F}\in O\left({G}\right)↔\left({F}\in \left(ℝ{↑}_{𝑝𝑚}ℝ\right)\wedge {G}\in \left(ℝ{↑}_{𝑝𝑚}ℝ\right)\wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left(\mathrm{dom}{F}\cap \left[{x},\mathrm{+\infty }\right)\right)\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {m}{G}\left({y}\right)\right)$