ello12

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

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

Metamath Proof Explorer

Theorem ello12

Proof