ello1

Description: Elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016)

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

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	breq1d	$⊢ f = F \to (f (y) \leq m \leftrightarrow F (y) \leq m)$
5	2 4	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)$
6	5	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)$
7		df-lo1	$⊢ \leq 𝑂 (1) = \{f \in (ℝ ↑_{𝑝𝑚} ℝ) \| \exists x \in ℝ \exists m \in ℝ \forall y \in (dom f \cap [x, +∞)) f (y) \leq m\}$
8	6 7	elrab2	$⊢ 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)$

Metamath Proof Explorer