elbigodm

Description: The domain of a function of order G(x) is a subset of the reals. (Contributed by AV, 18-May-2020)

		Ref	Expression
	Assertion	elbigodm	$⊢ F \in O (G) \to dom F \subseteq ℝ$

Step	Hyp	Ref	Expression
1		elbigo	$⊢ F \in O (G) \leftrightarrow (F \in (ℝ ↑_{𝑝𝑚} ℝ) \land G \in (ℝ ↑_{𝑝𝑚} ℝ) \land \exists x \in ℝ \exists m \in ℝ \forall y \in (dom F \cap [x, +∞)) F (y) \leq m G (y))$
2		reex	$⊢ ℝ \in V$
3	2 2	elpm2	$⊢ F \in (ℝ ↑_{𝑝𝑚} ℝ) \leftrightarrow (F : dom F ⟶ ℝ \land dom F \subseteq ℝ)$
4	3	simprbi	$⊢ F \in (ℝ ↑_{𝑝𝑚} ℝ) \to dom F \subseteq ℝ$
5	4	3ad2ant1	$⊢ (F \in (ℝ ↑_{𝑝𝑚} ℝ) \land G \in (ℝ ↑_{𝑝𝑚} ℝ) \land \exists x \in ℝ \exists m \in ℝ \forall y \in (dom F \cap [x, +∞)) F (y) \leq m G (y)) \to dom F \subseteq ℝ$
6	1 5	sylbi	$⊢ F \in O (G) \to dom F \subseteq ℝ$

Metamath Proof Explorer