elo12

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

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

Proof

Step	Hyp	Ref	Expression
1		cnex	$⊢ ℂ \in V$
2		reex	$⊢ ℝ \in V$
3		elpm2r	$⊢ ((ℂ \in V \land ℝ \in V) \land (F : A ⟶ ℂ \land A \subseteq ℝ)) \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
4	1 2 3	mpanl12	$⊢ (F : A ⟶ ℂ \land A \subseteq ℝ) \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
5		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)$
6	5	baib	$⊢ F \in (ℂ ↑_{𝑝𝑚} ℝ) \to (F \in 𝑂 (1) \leftrightarrow \exists x \in ℝ \exists m \in ℝ \forall y \in (dom F \cap [x, +∞)) \|F (y)\| \leq m)$
7	4 6	syl	$⊢ (F : A ⟶ ℂ \land A \subseteq ℝ) \to (F \in 𝑂 (1) \leftrightarrow \exists x \in ℝ \exists m \in ℝ \forall y \in (dom F \cap [x, +∞)) \|F (y)\| \leq m)$
8		elin	$⊢ y \in (dom F \cap [x, +∞)) \leftrightarrow (y \in dom F \land y \in [x, +∞))$
9		fdm	$⊢ F : A ⟶ ℂ \to dom F = A$
10	9	ad3antrrr	$⊢ (((F : A ⟶ ℂ \land A \subseteq ℝ) \land x \in ℝ) \land m \in ℝ) \to dom F = A$
11	10	eleq2d	$⊢ (((F : A ⟶ ℂ \land A \subseteq ℝ) \land x \in ℝ) \land m \in ℝ) \to (y \in dom F \leftrightarrow y \in A)$
12	11	anbi1d	$⊢ (((F : A ⟶ ℂ \land A \subseteq ℝ) \land x \in ℝ) \land m \in ℝ) \to ((y \in dom F \land y \in [x, +∞)) \leftrightarrow (y \in A \land y \in [x, +∞)))$
13		simpllr	$⊢ (((F : A ⟶ ℂ \land A \subseteq ℝ) \land x \in ℝ) \land m \in ℝ) \to A \subseteq ℝ$
14	13	sselda	$⊢ ((((F : A ⟶ ℂ \land A \subseteq ℝ) \land x \in ℝ) \land m \in ℝ) \land y \in A) \to y \in ℝ$
15		simpllr	$⊢ ((((F : A ⟶ ℂ \land A \subseteq ℝ) \land x \in ℝ) \land m \in ℝ) \land y \in A) \to x \in ℝ$
16		elicopnf	$⊢ x \in ℝ \to (y \in [x, +∞) \leftrightarrow (y \in ℝ \land x \leq y))$
17	15 16	syl	$⊢ ((((F : A ⟶ ℂ \land A \subseteq ℝ) \land x \in ℝ) \land m \in ℝ) \land y \in A) \to (y \in [x, +∞) \leftrightarrow (y \in ℝ \land x \leq y))$
18	14 17	mpbirand	$⊢ ((((F : A ⟶ ℂ \land A \subseteq ℝ) \land x \in ℝ) \land m \in ℝ) \land y \in A) \to (y \in [x, +∞) \leftrightarrow x \leq y)$
19	18	pm5.32da	$⊢ (((F : A ⟶ ℂ \land A \subseteq ℝ) \land x \in ℝ) \land m \in ℝ) \to ((y \in A \land y \in [x, +∞)) \leftrightarrow (y \in A \land x \leq y))$
20	12 19	bitrd	$⊢ (((F : A ⟶ ℂ \land A \subseteq ℝ) \land x \in ℝ) \land m \in ℝ) \to ((y \in dom F \land y \in [x, +∞)) \leftrightarrow (y \in A \land x \leq y))$
21	8 20	syl5bb	$⊢ (((F : A ⟶ ℂ \land A \subseteq ℝ) \land x \in ℝ) \land m \in ℝ) \to (y \in (dom F \cap [x, +∞)) \leftrightarrow (y \in A \land x \leq y))$
22	21	imbi1d	$⊢ (((F : A ⟶ ℂ \land A \subseteq ℝ) \land x \in ℝ) \land m \in ℝ) \to ((y \in (dom F \cap [x, +∞)) \to \|F (y)\| \leq m) \leftrightarrow ((y \in A \land x \leq y) \to \|F (y)\| \leq m))$
23		impexp	$⊢ ((y \in A \land x \leq y) \to \|F (y)\| \leq m) \leftrightarrow (y \in A \to (x \leq y \to \|F (y)\| \leq m))$
24	22 23	bitrdi	$⊢ (((F : A ⟶ ℂ \land A \subseteq ℝ) \land x \in ℝ) \land m \in ℝ) \to ((y \in (dom F \cap [x, +∞)) \to \|F (y)\| \leq m) \leftrightarrow (y \in A \to (x \leq y \to \|F (y)\| \leq m)))$
25	24	ralbidv2	$⊢ (((F : A ⟶ ℂ \land A \subseteq ℝ) \land x \in ℝ) \land m \in ℝ) \to (\forall y \in (dom F \cap [x, +∞)) \|F (y)\| \leq m \leftrightarrow \forall y \in A (x \leq y \to \|F (y)\| \leq m))$
26	25	rexbidva	$⊢ ((F : A ⟶ ℂ \land A \subseteq ℝ) \land x \in ℝ) \to (\exists m \in ℝ \forall y \in (dom F \cap [x, +∞)) \|F (y)\| \leq m \leftrightarrow \exists m \in ℝ \forall y \in A (x \leq y \to \|F (y)\| \leq m))$
27	26	rexbidva	$⊢ (F : A ⟶ ℂ \land A \subseteq ℝ) \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 A (x \leq y \to \|F (y)\| \leq m))$
28	7 27	bitrd	$⊢ (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))$

Metamath Proof Explorer

Theorem elo12

Proof