Metamath Proof Explorer

Theorem elbigo

Description: Properties of a function of order G(x). (Contributed by AV, 16-May-2020)

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

Proof

Step	Hyp	Ref	Expression
1		bigoval	$⊢ G \in (ℝ ↑_{𝑝𝑚} ℝ) \to O (G) = \{f \in (ℝ ↑_{𝑝𝑚} ℝ) \| \exists x \in ℝ \exists m \in ℝ \forall y \in (dom f \cap [x, +∞)) f (y) \leq m G (y)\}$
2	1	eleq2d	$⊢ G \in (ℝ ↑_{𝑝𝑚} ℝ) \to (F \in O (G) \leftrightarrow F \in \{f \in (ℝ ↑_{𝑝𝑚} ℝ) \| \exists x \in ℝ \exists m \in ℝ \forall y \in (dom f \cap [x, +∞)) f (y) \leq m G (y)\})$
3		dmeq	$⊢ f = F \to dom f = dom F$
4	3	ineq1d	$⊢ f = F \to dom f \cap [x, +∞) = dom F \cap [x, +∞)$
5		fveq1	$⊢ f = F \to f (y) = F (y)$
6	5	breq1d	$⊢ f = F \to (f (y) \leq m G (y) \leftrightarrow F (y) \leq m G (y))$
7	4 6	raleqbidv	$⊢ f = F \to (\forall y \in (dom f \cap [x, +∞)) f (y) \leq m G (y) \leftrightarrow \forall y \in (dom F \cap [x, +∞)) F (y) \leq m G (y))$
8	7	2rexbidv	$⊢ f = F \to (\exists x \in ℝ \exists m \in ℝ \forall y \in (dom f \cap [x, +∞)) f (y) \leq m G (y) \leftrightarrow \exists x \in ℝ \exists m \in ℝ \forall y \in (dom F \cap [x, +∞)) F (y) \leq m G (y))$
9	8	elrab	$⊢ F \in \{f \in (ℝ ↑_{𝑝𝑚} ℝ) \| \exists x \in ℝ \exists m \in ℝ \forall y \in (dom f \cap [x, +∞)) f (y) \leq m G (y)\} \leftrightarrow (F \in (ℝ ↑_{𝑝𝑚} ℝ) \land \exists x \in ℝ \exists m \in ℝ \forall y \in (dom F \cap [x, +∞)) F (y) \leq m G (y))$
10	2 9	syl6bb	$⊢ G \in (ℝ ↑_{𝑝𝑚} ℝ) \to (F \in O (G) \leftrightarrow (F \in (ℝ ↑_{𝑝𝑚} ℝ) \land \exists x \in ℝ \exists m \in ℝ \forall y \in (dom F \cap [x, +∞)) F (y) \leq m G (y)))$
11	10	pm5.32i	$⊢ (G \in (ℝ ↑_{𝑝𝑚} ℝ) \land F \in O (G)) \leftrightarrow (G \in (ℝ ↑_{𝑝𝑚} ℝ) \land (F \in (ℝ ↑_{𝑝𝑚} ℝ) \land \exists x \in ℝ \exists m \in ℝ \forall y \in (dom F \cap [x, +∞)) F (y) \leq m G (y)))$
12		elbigofrcl	$⊢ F \in O (G) \to G \in (ℝ ↑_{𝑝𝑚} ℝ)$
13	12	pm4.71ri	$⊢ F \in O (G) \leftrightarrow (G \in (ℝ ↑_{𝑝𝑚} ℝ) \land F \in O (G))$
14		3anan12	$⊢ (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)) \leftrightarrow (G \in (ℝ ↑_{𝑝𝑚} ℝ) \land (F \in (ℝ ↑_{𝑝𝑚} ℝ) \land \exists x \in ℝ \exists m \in ℝ \forall y \in (dom F \cap [x, +∞)) F (y) \leq m G (y)))$
15	11 13 14	3bitr4i	$⊢ 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))$