o1dm

Description: An eventually bounded function's domain is a subset of the reals. (Contributed by Mario Carneiro, 15-Sep-2014)

		Ref	Expression
	Assertion	o1dm	$⊢ F \in 𝑂 (1) \to dom F \subseteq ℝ$

Step	Hyp	Ref	Expression
1		elo1	$⊢ F \in 𝑂 (1) \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} ℝ) \land \exists x \in ℝ \exists m \in ℝ \forall y \in (dom F \cap [x, +∞)) \|F (y)\| \leq m)$
2	1	simplbi	$⊢ F \in 𝑂 (1) \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
3		cnex	$⊢ ℂ \in V$
4		reex	$⊢ ℝ \in V$
5	3 4	elpm2	$⊢ F \in (ℂ ↑_{𝑝𝑚} ℝ) \leftrightarrow (F : dom F ⟶ ℂ \land dom F \subseteq ℝ)$
6	5	simprbi	$⊢ F \in (ℂ ↑_{𝑝𝑚} ℝ) \to dom F \subseteq ℝ$
7	2 6	syl	$⊢ F \in 𝑂 (1) \to dom F \subseteq ℝ$

Metamath Proof Explorer