elo1

Description: Elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 15-Sep-2014)

		Ref	Expression
	Assertion	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)$

Step	Hyp	Ref	Expression
1		dmeq	$⊢ f = F \to dom f = dom F$
2	1	ineq1d	$⊢ f = F \to dom f \cap [x, +∞) = dom F \cap [x, +∞)$
3		fveq1	$⊢ f = F \to f (y) = F (y)$
4	3	fveq2d	$⊢ f = F \to \|f (y)\| = \|F (y)\|$
5	4	breq1d	$⊢ f = F \to (\|f (y)\| \leq m \leftrightarrow \|F (y)\| \leq m)$
6	2 5	raleqbidv	$⊢ f = F \to (\forall y \in (dom f \cap [x, +∞)) \|f (y)\| \leq m \leftrightarrow \forall y \in (dom F \cap [x, +∞)) \|F (y)\| \leq m)$
7	6	2rexbidv	$⊢ f = F \to (\exists x \in ℝ \exists m \in ℝ \forall y \in (dom f \cap [x, +∞)) \|f (y)\| \leq m \leftrightarrow \exists x \in ℝ \exists m \in ℝ \forall y \in (dom F \cap [x, +∞)) \|F (y)\| \leq m)$
8		df-o1	$⊢ 𝑂 (1) = \{f \in (ℂ ↑_{𝑝𝑚} ℝ) \| \exists x \in ℝ \exists m \in ℝ \forall y \in (dom f \cap [x, +∞)) \|f (y)\| \leq m\}$
9	7 8	elrab2	$⊢ F \in 𝑂 (1) \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} ℝ) \land \exists x \in ℝ \exists m \in ℝ \forall y \in (dom F \cap [x, +∞)) \|F (y)\| \leq m)$

Metamath Proof Explorer