o1bdd

Description: The defining property of an eventually bounded function. (Contributed by Mario Carneiro, 15-Sep-2014)

		Ref	Expression
	Assertion	o1bdd	$⊢ (F \in 𝑂 (1) \land F : A ⟶ ℂ) \to \exists x \in ℝ \exists m \in ℝ \forall y \in A (x \leq y \to \|F (y)\| \leq m)$

Step	Hyp	Ref	Expression
1		simpl	$⊢ (F \in 𝑂 (1) \land F : A ⟶ ℂ) \to F \in 𝑂 (1)$
2		simpr	$⊢ (F \in 𝑂 (1) \land F : A ⟶ ℂ) \to F : A ⟶ ℂ$
3		fdm	$⊢ F : A ⟶ ℂ \to dom F = A$
4	3	adantl	$⊢ (F \in 𝑂 (1) \land F : A ⟶ ℂ) \to dom F = A$
5		o1dm	$⊢ F \in 𝑂 (1) \to dom F \subseteq ℝ$
6	5	adantr	$⊢ (F \in 𝑂 (1) \land F : A ⟶ ℂ) \to dom F \subseteq ℝ$
7	4 6	eqsstrrd	$⊢ (F \in 𝑂 (1) \land F : A ⟶ ℂ) \to A \subseteq ℝ$
8		elo12	$⊢ (F : A ⟶ ℂ \land A \subseteq ℝ) \to (F \in 𝑂 (1) \leftrightarrow \exists x \in ℝ \exists m \in ℝ \forall y \in A (x \leq y \to \|F (y)\| \leq m))$
9	2 7 8	syl2anc	$⊢ (F \in 𝑂 (1) \land F : A ⟶ ℂ) \to (F \in 𝑂 (1) \leftrightarrow \exists x \in ℝ \exists m \in ℝ \forall y \in A (x \leq y \to \|F (y)\| \leq m))$
10	1 9	mpbid	$⊢ (F \in 𝑂 (1) \land F : A ⟶ ℂ) \to \exists x \in ℝ \exists m \in ℝ \forall y \in A (x \leq y \to \|F (y)\| \leq m)$

Metamath Proof Explorer