elbigoimp

Description: The defining property of a function of order G(x). (Contributed by AV, 18-May-2020)

		Ref	Expression
	Assertion	elbigoimp	$⊢ (F \in O (G) \land F : A ⟶ ℝ \land A \subseteq dom G) \to \exists x \in ℝ \exists m \in ℝ \forall y \in A (x \leq y \to F (y) \leq m G (y))$

Step	Hyp	Ref	Expression
1		simp1	$⊢ (F \in O (G) \land F : A ⟶ ℝ \land A \subseteq dom G) \to F \in O (G)$
2		elbigofrcl	$⊢ F \in O (G) \to G \in (ℝ ↑_{𝑝𝑚} ℝ)$
3		reex	$⊢ ℝ \in V$
4	3 3	elpm2	$⊢ G \in (ℝ ↑_{𝑝𝑚} ℝ) \leftrightarrow (G : dom G ⟶ ℝ \land dom G \subseteq ℝ)$
5	2 4	sylib	$⊢ F \in O (G) \to (G : dom G ⟶ ℝ \land dom G \subseteq ℝ)$
6	5	3ad2ant1	$⊢ (F \in O (G) \land F : A ⟶ ℝ \land A \subseteq dom G) \to (G : dom G ⟶ ℝ \land dom G \subseteq ℝ)$
7		3simpc	$⊢ (F \in O (G) \land F : A ⟶ ℝ \land A \subseteq dom G) \to (F : A ⟶ ℝ \land A \subseteq dom G)$
8		elbigo2	$⊢ ((G : dom G ⟶ ℝ \land dom G \subseteq ℝ) \land (F : A ⟶ ℝ \land A \subseteq dom G)) \to (F \in O (G) \leftrightarrow \exists x \in ℝ \exists m \in ℝ \forall y \in A (x \leq y \to F (y) \leq m G (y)))$
9	6 7 8	syl2anc	$⊢ (F \in O (G) \land F : A ⟶ ℝ \land A \subseteq dom G) \to (F \in O (G) \leftrightarrow \exists x \in ℝ \exists m \in ℝ \forall y \in A (x \leq y \to F (y) \leq m G (y)))$
10	1 9	mpbid	$⊢ (F \in O (G) \land F : A ⟶ ℝ \land A \subseteq dom G) \to \exists x \in ℝ \exists m \in ℝ \forall y \in A (x \leq y \to F (y) \leq m G (y))$

Metamath Proof Explorer