# Metamath Proof Explorer

## Theorem elbigof

Description: A function of order G(x) is a function. (Contributed by AV, 18-May-2020)

Ref Expression
Assertion elbigof ${⊢}{F}\in O\left({G}\right)\to {F}:\mathrm{dom}{F}⟶ℝ$

### Proof

Step Hyp Ref Expression
1 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)$
2 reex ${⊢}ℝ\in \mathrm{V}$
3 2 2 elpm2 ${⊢}{F}\in \left(ℝ{↑}_{𝑝𝑚}ℝ\right)↔\left({F}:\mathrm{dom}{F}⟶ℝ\wedge \mathrm{dom}{F}\subseteq ℝ\right)$
4 3 simplbi ${⊢}{F}\in \left(ℝ{↑}_{𝑝𝑚}ℝ\right)\to {F}:\mathrm{dom}{F}⟶ℝ$
5 4 3ad2ant1 ${⊢}\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)\to {F}:\mathrm{dom}{F}⟶ℝ$
6 1 5 sylbi ${⊢}{F}\in O\left({G}\right)\to {F}:\mathrm{dom}{F}⟶ℝ$