lo1dm

Description: An eventually upper bounded function's domain is a subset of the reals. (Contributed by Mario Carneiro, 26-May-2016)

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

Step	Hyp	Ref	Expression
1		ello1	$⊢ F \in \leq 𝑂 (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 \leq 𝑂 (1) \to F \in (ℝ ↑_{𝑝𝑚} ℝ)$
3		reex	$⊢ ℝ \in V$
4	3 3	elpm2	$⊢ F \in (ℝ ↑_{𝑝𝑚} ℝ) \leftrightarrow (F : dom F ⟶ ℝ \land dom F \subseteq ℝ)$
5	4	simprbi	$⊢ F \in (ℝ ↑_{𝑝𝑚} ℝ) \to dom F \subseteq ℝ$
6	2 5	syl	$⊢ F \in \leq 𝑂 (1) \to dom F \subseteq ℝ$

Metamath Proof Explorer