lo1bdd2

Description: If an eventually bounded function is bounded on every interval A i^i ( -oo , y ) by a function M ( y ) , then the function is bounded on the whole domain. (Contributed by Mario Carneiro, 9-Apr-2016)

	Ref	Expression
Hypotheses	lo1bdd2.1	$⊢ φ \to A \subseteq ℝ$
	lo1bdd2.2	$⊢ φ \to C \in ℝ$
	lo1bdd2.3	$⊢ (φ \land x \in A) \to B \in ℝ$
	lo1bdd2.4	$⊢ φ \to (x \in A ⟼ B) \in \leq 𝑂 (1)$
	lo1bdd2.5	$⊢ (φ \land (y \in ℝ \land C \leq y)) \to M \in ℝ$
	lo1bdd2.6	$⊢ ((φ \land x \in A) \land ((y \in ℝ \land C \leq y) \land x < y)) \to B \leq M$
Assertion	lo1bdd2	$⊢ φ \to \exists m \in ℝ \forall x \in A B \leq m$

Proof

Step	Hyp	Ref	Expression
1		lo1bdd2.1	$⊢ φ \to A \subseteq ℝ$
2		lo1bdd2.2	$⊢ φ \to C \in ℝ$
3		lo1bdd2.3	$⊢ (φ \land x \in A) \to B \in ℝ$
4		lo1bdd2.4	$⊢ φ \to (x \in A ⟼ B) \in \leq 𝑂 (1)$
5		lo1bdd2.5	$⊢ (φ \land (y \in ℝ \land C \leq y)) \to M \in ℝ$
6		lo1bdd2.6	$⊢ ((φ \land x \in A) \land ((y \in ℝ \land C \leq y) \land x < y)) \to B \leq M$
7	1 3 2	ello1mpt2	$⊢ φ \to ((x \in A ⟼ B) \in \leq 𝑂 (1) \leftrightarrow \exists y \in [C, +∞) \exists n \in ℝ \forall x \in A (y \leq x \to B \leq n))$
8	4 7	mpbid	$⊢ φ \to \exists y \in [C, +∞) \exists n \in ℝ \forall x \in A (y \leq x \to B \leq n)$
9		elicopnf	$⊢ C \in ℝ \to (y \in [C, +∞) \leftrightarrow (y \in ℝ \land C \leq y))$
10	2 9	syl	$⊢ φ \to (y \in [C, +∞) \leftrightarrow (y \in ℝ \land C \leq y))$
11	10	biimpa	$⊢ (φ \land y \in [C, +∞)) \to (y \in ℝ \land C \leq y)$
12	11 5	syldan	$⊢ (φ \land y \in [C, +∞)) \to M \in ℝ$
13	12	ad2antrr	$⊢ (((φ \land y \in [C, +∞)) \land (n \in ℝ \land \forall x \in A (y \leq x \to B \leq n))) \land n \leq M) \to M \in ℝ$
14		simplrl	$⊢ (((φ \land y \in [C, +∞)) \land (n \in ℝ \land \forall x \in A (y \leq x \to B \leq n))) \land \neg n \leq M) \to n \in ℝ$
15	13 14	ifclda	$⊢ ((φ \land y \in [C, +∞)) \land (n \in ℝ \land \forall x \in A (y \leq x \to B \leq n))) \to if (n \leq M, M, n) \in ℝ$
16	1	ad2antrr	$⊢ ((φ \land y \in [C, +∞)) \land n \in ℝ) \to A \subseteq ℝ$
17	16	sselda	$⊢ (((φ \land y \in [C, +∞)) \land n \in ℝ) \land x \in A) \to x \in ℝ$
18	11	simpld	$⊢ (φ \land y \in [C, +∞)) \to y \in ℝ$
19	18	ad2antrr	$⊢ (((φ \land y \in [C, +∞)) \land n \in ℝ) \land x \in A) \to y \in ℝ$
20	17 19	ltnled	$⊢ (((φ \land y \in [C, +∞)) \land n \in ℝ) \land x \in A) \to (x < y \leftrightarrow \neg y \leq x)$
21	6	expr	$⊢ ((φ \land x \in A) \land (y \in ℝ \land C \leq y)) \to (x < y \to B \leq M)$
22	21	an32s	$⊢ ((φ \land (y \in ℝ \land C \leq y)) \land x \in A) \to (x < y \to B \leq M)$
23	11 22	syldanl	$⊢ ((φ \land y \in [C, +∞)) \land x \in A) \to (x < y \to B \leq M)$
24	23	adantlr	$⊢ (((φ \land y \in [C, +∞)) \land n \in ℝ) \land x \in A) \to (x < y \to B \leq M)$
25		simplr	$⊢ (((φ \land y \in [C, +∞)) \land n \in ℝ) \land x \in A) \to n \in ℝ$
26	12	ad2antrr	$⊢ (((φ \land y \in [C, +∞)) \land n \in ℝ) \land x \in A) \to M \in ℝ$
27		max2	$⊢ (n \in ℝ \land M \in ℝ) \to M \leq if (n \leq M, M, n)$
28	25 26 27	syl2anc	$⊢ (((φ \land y \in [C, +∞)) \land n \in ℝ) \land x \in A) \to M \leq if (n \leq M, M, n)$
29	3	ad4ant14	$⊢ (((φ \land y \in [C, +∞)) \land n \in ℝ) \land x \in A) \to B \in ℝ$
30	12	ad5ant12	$⊢ ((((φ \land y \in [C, +∞)) \land n \in ℝ) \land x \in A) \land n \leq M) \to M \in ℝ$
31		simpllr	$⊢ ((((φ \land y \in [C, +∞)) \land n \in ℝ) \land x \in A) \land \neg n \leq M) \to n \in ℝ$
32	30 31	ifclda	$⊢ (((φ \land y \in [C, +∞)) \land n \in ℝ) \land x \in A) \to if (n \leq M, M, n) \in ℝ$
33		letr	$⊢ (B \in ℝ \land M \in ℝ \land if (n \leq M, M, n) \in ℝ) \to ((B \leq M \land M \leq if (n \leq M, M, n)) \to B \leq if (n \leq M, M, n))$
34	29 26 32 33	syl3anc	$⊢ (((φ \land y \in [C, +∞)) \land n \in ℝ) \land x \in A) \to ((B \leq M \land M \leq if (n \leq M, M, n)) \to B \leq if (n \leq M, M, n))$
35	28 34	mpan2d	$⊢ (((φ \land y \in [C, +∞)) \land n \in ℝ) \land x \in A) \to (B \leq M \to B \leq if (n \leq M, M, n))$
36	24 35	syld	$⊢ (((φ \land y \in [C, +∞)) \land n \in ℝ) \land x \in A) \to (x < y \to B \leq if (n \leq M, M, n))$
37	20 36	sylbird	$⊢ (((φ \land y \in [C, +∞)) \land n \in ℝ) \land x \in A) \to (\neg y \leq x \to B \leq if (n \leq M, M, n))$
38		max1	$⊢ (n \in ℝ \land M \in ℝ) \to n \leq if (n \leq M, M, n)$
39	25 26 38	syl2anc	$⊢ (((φ \land y \in [C, +∞)) \land n \in ℝ) \land x \in A) \to n \leq if (n \leq M, M, n)$
40		letr	$⊢ (B \in ℝ \land n \in ℝ \land if (n \leq M, M, n) \in ℝ) \to ((B \leq n \land n \leq if (n \leq M, M, n)) \to B \leq if (n \leq M, M, n))$
41	29 25 32 40	syl3anc	$⊢ (((φ \land y \in [C, +∞)) \land n \in ℝ) \land x \in A) \to ((B \leq n \land n \leq if (n \leq M, M, n)) \to B \leq if (n \leq M, M, n))$
42	39 41	mpan2d	$⊢ (((φ \land y \in [C, +∞)) \land n \in ℝ) \land x \in A) \to (B \leq n \to B \leq if (n \leq M, M, n))$
43	37 42	jad	$⊢ (((φ \land y \in [C, +∞)) \land n \in ℝ) \land x \in A) \to ((y \leq x \to B \leq n) \to B \leq if (n \leq M, M, n))$
44	43	ralimdva	$⊢ ((φ \land y \in [C, +∞)) \land n \in ℝ) \to (\forall x \in A (y \leq x \to B \leq n) \to \forall x \in A B \leq if (n \leq M, M, n))$
45	44	impr	$⊢ ((φ \land y \in [C, +∞)) \land (n \in ℝ \land \forall x \in A (y \leq x \to B \leq n))) \to \forall x \in A B \leq if (n \leq M, M, n)$
46		brralrspcev	$⊢ (if (n \leq M, M, n) \in ℝ \land \forall x \in A B \leq if (n \leq M, M, n)) \to \exists m \in ℝ \forall x \in A B \leq m$
47	15 45 46	syl2anc	$⊢ ((φ \land y \in [C, +∞)) \land (n \in ℝ \land \forall x \in A (y \leq x \to B \leq n))) \to \exists m \in ℝ \forall x \in A B \leq m$
48	47	expr	$⊢ ((φ \land y \in [C, +∞)) \land n \in ℝ) \to (\forall x \in A (y \leq x \to B \leq n) \to \exists m \in ℝ \forall x \in A B \leq m)$
49	48	rexlimdva	$⊢ (φ \land y \in [C, +∞)) \to (\exists n \in ℝ \forall x \in A (y \leq x \to B \leq n) \to \exists m \in ℝ \forall x \in A B \leq m)$
50	49	rexlimdva	$⊢ φ \to (\exists y \in [C, +∞) \exists n \in ℝ \forall x \in A (y \leq x \to B \leq n) \to \exists m \in ℝ \forall x \in A B \leq m)$
51	8 50	mpd	$⊢ φ \to \exists m \in ℝ \forall x \in A B \leq m$

Metamath Proof Explorer

Theorem lo1bdd2

Proof