lo1resb

Description: The restriction of a function to an unbounded-above interval is eventually upper bounded iff the original is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016)

	Ref	Expression
Hypotheses	lo1resb.1	$⊢ φ \to F : A ⟶ ℝ$
	lo1resb.2	$⊢ φ \to A \subseteq ℝ$
	lo1resb.3	$⊢ φ \to B \in ℝ$
Assertion	lo1resb	$⊢ φ \to (F \in \leq 𝑂 (1) \leftrightarrow {F ↾}_{[B, +∞)} \in \leq 𝑂 (1))$

Proof

Step	Hyp	Ref	Expression
1		lo1resb.1	$⊢ φ \to F : A ⟶ ℝ$
2		lo1resb.2	$⊢ φ \to A \subseteq ℝ$
3		lo1resb.3	$⊢ φ \to B \in ℝ$
4		lo1res	$⊢ F \in \leq 𝑂 (1) \to {F ↾}_{[B, +∞)} \in \leq 𝑂 (1)$
5	1	feqmptd	$⊢ φ \to F = (x \in A ⟼ F (x))$
6	5	reseq1d	$⊢ φ \to {F ↾}_{[B, +∞)} = {(x \in A ⟼ F (x)) ↾}_{[B, +∞)}$
7		resmpt3	$⊢ {(x \in A ⟼ F (x)) ↾}_{[B, +∞)} = (x \in (A \cap [B, +∞)) ⟼ F (x))$
8	6 7	eqtrdi	$⊢ φ \to {F ↾}_{[B, +∞)} = (x \in (A \cap [B, +∞)) ⟼ F (x))$
9	8	eleq1d	$⊢ φ \to ({F ↾}_{[B, +∞)} \in \leq 𝑂 (1) \leftrightarrow (x \in (A \cap [B, +∞)) ⟼ F (x)) \in \leq 𝑂 (1))$
10		inss1	$⊢ A \cap [B, +∞) \subseteq A$
11	10 2	sstrid	$⊢ φ \to A \cap [B, +∞) \subseteq ℝ$
12		elinel1	$⊢ x \in (A \cap [B, +∞)) \to x \in A$
13		ffvelcdm	$⊢ (F : A ⟶ ℝ \land x \in A) \to F (x) \in ℝ$
14	1 12 13	syl2an	$⊢ (φ \land x \in (A \cap [B, +∞))) \to F (x) \in ℝ$
15	11 14	ello1mpt	$⊢ φ \to ((x \in (A \cap [B, +∞)) ⟼ F (x)) \in \leq 𝑂 (1) \leftrightarrow \exists y \in ℝ \exists z \in ℝ \forall x \in (A \cap [B, +∞)) (y \leq x \to F (x) \leq z))$
16		elin	$⊢ x \in (A \cap [B, +∞)) \leftrightarrow (x \in A \land x \in [B, +∞))$
17	16	imbi1i	$⊢ (x \in (A \cap [B, +∞)) \to (y \leq x \to F (x) \leq z)) \leftrightarrow ((x \in A \land x \in [B, +∞)) \to (y \leq x \to F (x) \leq z))$
18		impexp	$⊢ ((x \in A \land x \in [B, +∞)) \to (y \leq x \to F (x) \leq z)) \leftrightarrow (x \in A \to (x \in [B, +∞) \to (y \leq x \to F (x) \leq z)))$
19	17 18	bitri	$⊢ (x \in (A \cap [B, +∞)) \to (y \leq x \to F (x) \leq z)) \leftrightarrow (x \in A \to (x \in [B, +∞) \to (y \leq x \to F (x) \leq z)))$
20		impexp	$⊢ ((x \in [B, +∞) \land y \leq x) \to F (x) \leq z) \leftrightarrow (x \in [B, +∞) \to (y \leq x \to F (x) \leq z))$
21	3	ad2antrr	$⊢ ((φ \land (y \in ℝ \land z \in ℝ)) \land x \in A) \to B \in ℝ$
22	2	adantr	$⊢ (φ \land (y \in ℝ \land z \in ℝ)) \to A \subseteq ℝ$
23	22	sselda	$⊢ ((φ \land (y \in ℝ \land z \in ℝ)) \land x \in A) \to x \in ℝ$
24		elicopnf	$⊢ B \in ℝ \to (x \in [B, +∞) \leftrightarrow (x \in ℝ \land B \leq x))$
25	24	baibd	$⊢ (B \in ℝ \land x \in ℝ) \to (x \in [B, +∞) \leftrightarrow B \leq x)$
26	21 23 25	syl2anc	$⊢ ((φ \land (y \in ℝ \land z \in ℝ)) \land x \in A) \to (x \in [B, +∞) \leftrightarrow B \leq x)$
27	26	anbi1d	$⊢ ((φ \land (y \in ℝ \land z \in ℝ)) \land x \in A) \to ((x \in [B, +∞) \land y \leq x) \leftrightarrow (B \leq x \land y \leq x))$
28		simplrl	$⊢ ((φ \land (y \in ℝ \land z \in ℝ)) \land x \in A) \to y \in ℝ$
29		maxle	$⊢ (B \in ℝ \land y \in ℝ \land x \in ℝ) \to (if (B \leq y, y, B) \leq x \leftrightarrow (B \leq x \land y \leq x))$
30	21 28 23 29	syl3anc	$⊢ ((φ \land (y \in ℝ \land z \in ℝ)) \land x \in A) \to (if (B \leq y, y, B) \leq x \leftrightarrow (B \leq x \land y \leq x))$
31	27 30	bitr4d	$⊢ ((φ \land (y \in ℝ \land z \in ℝ)) \land x \in A) \to ((x \in [B, +∞) \land y \leq x) \leftrightarrow if (B \leq y, y, B) \leq x)$
32	31	imbi1d	$⊢ ((φ \land (y \in ℝ \land z \in ℝ)) \land x \in A) \to (((x \in [B, +∞) \land y \leq x) \to F (x) \leq z) \leftrightarrow (if (B \leq y, y, B) \leq x \to F (x) \leq z))$
33	20 32	bitr3id	$⊢ ((φ \land (y \in ℝ \land z \in ℝ)) \land x \in A) \to ((x \in [B, +∞) \to (y \leq x \to F (x) \leq z)) \leftrightarrow (if (B \leq y, y, B) \leq x \to F (x) \leq z))$
34	33	pm5.74da	$⊢ (φ \land (y \in ℝ \land z \in ℝ)) \to ((x \in A \to (x \in [B, +∞) \to (y \leq x \to F (x) \leq z))) \leftrightarrow (x \in A \to (if (B \leq y, y, B) \leq x \to F (x) \leq z)))$
35	19 34	bitrid	$⊢ (φ \land (y \in ℝ \land z \in ℝ)) \to ((x \in (A \cap [B, +∞)) \to (y \leq x \to F (x) \leq z)) \leftrightarrow (x \in A \to (if (B \leq y, y, B) \leq x \to F (x) \leq z)))$
36	35	ralbidv2	$⊢ (φ \land (y \in ℝ \land z \in ℝ)) \to (\forall x \in (A \cap [B, +∞)) (y \leq x \to F (x) \leq z) \leftrightarrow \forall x \in A (if (B \leq y, y, B) \leq x \to F (x) \leq z))$
37	1	adantr	$⊢ (φ \land (y \in ℝ \land z \in ℝ)) \to F : A ⟶ ℝ$
38		simprl	$⊢ (φ \land (y \in ℝ \land z \in ℝ)) \to y \in ℝ$
39	3	adantr	$⊢ (φ \land (y \in ℝ \land z \in ℝ)) \to B \in ℝ$
40	38 39	ifcld	$⊢ (φ \land (y \in ℝ \land z \in ℝ)) \to if (B \leq y, y, B) \in ℝ$
41		simprr	$⊢ (φ \land (y \in ℝ \land z \in ℝ)) \to z \in ℝ$
42		ello12r	$⊢ ((F : A ⟶ ℝ \land A \subseteq ℝ) \land (if (B \leq y, y, B) \in ℝ \land z \in ℝ) \land \forall x \in A (if (B \leq y, y, B) \leq x \to F (x) \leq z)) \to F \in \leq 𝑂 (1)$
43	42	3expia	$⊢ ((F : A ⟶ ℝ \land A \subseteq ℝ) \land (if (B \leq y, y, B) \in ℝ \land z \in ℝ)) \to (\forall x \in A (if (B \leq y, y, B) \leq x \to F (x) \leq z) \to F \in \leq 𝑂 (1))$
44	37 22 40 41 43	syl22anc	$⊢ (φ \land (y \in ℝ \land z \in ℝ)) \to (\forall x \in A (if (B \leq y, y, B) \leq x \to F (x) \leq z) \to F \in \leq 𝑂 (1))$
45	36 44	sylbid	$⊢ (φ \land (y \in ℝ \land z \in ℝ)) \to (\forall x \in (A \cap [B, +∞)) (y \leq x \to F (x) \leq z) \to F \in \leq 𝑂 (1))$
46	45	rexlimdvva	$⊢ φ \to (\exists y \in ℝ \exists z \in ℝ \forall x \in (A \cap [B, +∞)) (y \leq x \to F (x) \leq z) \to F \in \leq 𝑂 (1))$
47	15 46	sylbid	$⊢ φ \to ((x \in (A \cap [B, +∞)) ⟼ F (x)) \in \leq 𝑂 (1) \to F \in \leq 𝑂 (1))$
48	9 47	sylbid	$⊢ φ \to ({F ↾}_{[B, +∞)} \in \leq 𝑂 (1) \to F \in \leq 𝑂 (1))$
49	4 48	impbid2	$⊢ φ \to (F \in \leq 𝑂 (1) \leftrightarrow {F ↾}_{[B, +∞)} \in \leq 𝑂 (1))$

Metamath Proof Explorer

Theorem lo1resb

Proof