Theorem 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	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	lo1bdd2.2	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	lo1bdd2.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
	lo1bdd2.4	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) )
	lo1bdd2.5	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦 ) ) → 𝑀 ∈ ℝ )
	lo1bdd2.6	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ( ( 𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝐵 ≤ 𝑀 )
Assertion	lo1bdd2	⊢ ( 𝜑 → ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑚 )

Proof

Step	Hyp	Ref	Expression
1		lo1bdd2.1	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2		lo1bdd2.2	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
3		lo1bdd2.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
4		lo1bdd2.4	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) )
5		lo1bdd2.5	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦 ) ) → 𝑀 ∈ ℝ )
6		lo1bdd2.6	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ( ( 𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝐵 ≤ 𝑀 )
7	1 3 2	ello1mpt2	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ↔ ∃ 𝑦 ∈ ( 𝐶 [,) +∞ ) ∃ 𝑛 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛 ) ) )
8	4 7	mpbid	⊢ ( 𝜑 → ∃ 𝑦 ∈ ( 𝐶 [,) +∞ ) ∃ 𝑛 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛 ) )
9		elicopnf	⊢ ( 𝐶 ∈ ℝ → ( 𝑦 ∈ ( 𝐶 [,) +∞ ) ↔ ( 𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦 ) ) )
10	2 9	syl	⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐶 [,) +∞ ) ↔ ( 𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦 ) ) )
11	10	biimpa	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 [,) +∞ ) ) → ( 𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦 ) )
12	11 5	syldan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 [,) +∞ ) ) → 𝑀 ∈ ℝ )
13	12	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 [,) +∞ ) ) ∧ ( 𝑛 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛 ) ) ) ∧ 𝑛 ≤ 𝑀 ) → 𝑀 ∈ ℝ )
14		simplrl	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 [,) +∞ ) ) ∧ ( 𝑛 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛 ) ) ) ∧ ¬ 𝑛 ≤ 𝑀 ) → 𝑛 ∈ ℝ )
15	13 14	ifclda	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 [,) +∞ ) ) ∧ ( 𝑛 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛 ) ) ) → if ( 𝑛 ≤ 𝑀 , 𝑀 , 𝑛 ) ∈ ℝ )
16	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 [,) +∞ ) ) ∧ 𝑛 ∈ ℝ ) → 𝐴 ⊆ ℝ )
17	16	sselda	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 [,) +∞ ) ) ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
18	11	simpld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 [,) +∞ ) ) → 𝑦 ∈ ℝ )
19	18	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 [,) +∞ ) ) ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ ℝ )
20	17 19	ltnled	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 [,) +∞ ) ) ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 < 𝑦 ↔ ¬ 𝑦 ≤ 𝑥 ) )
21	6	expr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦 ) ) → ( 𝑥 < 𝑦 → 𝐵 ≤ 𝑀 ) )
22	21	an32s	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝐶 ≤ 𝑦 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 < 𝑦 → 𝐵 ≤ 𝑀 ) )
23	11 22	syldanl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 < 𝑦 → 𝐵 ≤ 𝑀 ) )
24	23	adantlr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 [,) +∞ ) ) ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 < 𝑦 → 𝐵 ≤ 𝑀 ) )
25		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 [,) +∞ ) ) ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝑛 ∈ ℝ )
26	12	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 [,) +∞ ) ) ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝑀 ∈ ℝ )
27		max2	⊢ ( ( 𝑛 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → 𝑀 ≤ if ( 𝑛 ≤ 𝑀 , 𝑀 , 𝑛 ) )
28	25 26 27	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 [,) +∞ ) ) ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝑀 ≤ if ( 𝑛 ≤ 𝑀 , 𝑀 , 𝑛 ) )
29	3	ad4ant14	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 [,) +∞ ) ) ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
30	12	ad3antrrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 [,) +∞ ) ) ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ≤ 𝑀 ) → 𝑀 ∈ ℝ )
31		simpllr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 [,) +∞ ) ) ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ 𝑛 ≤ 𝑀 ) → 𝑛 ∈ ℝ )
32	30 31	ifclda	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 [,) +∞ ) ) ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑛 ≤ 𝑀 , 𝑀 , 𝑛 ) ∈ ℝ )
33		letr	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ if ( 𝑛 ≤ 𝑀 , 𝑀 , 𝑛 ) ∈ ℝ ) → ( ( 𝐵 ≤ 𝑀 ∧ 𝑀 ≤ if ( 𝑛 ≤ 𝑀 , 𝑀 , 𝑛 ) ) → 𝐵 ≤ if ( 𝑛 ≤ 𝑀 , 𝑀 , 𝑛 ) ) )
34	29 26 32 33	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 [,) +∞ ) ) ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐵 ≤ 𝑀 ∧ 𝑀 ≤ if ( 𝑛 ≤ 𝑀 , 𝑀 , 𝑛 ) ) → 𝐵 ≤ if ( 𝑛 ≤ 𝑀 , 𝑀 , 𝑛 ) ) )
35	28 34	mpan2d	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 [,) +∞ ) ) ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ≤ 𝑀 → 𝐵 ≤ if ( 𝑛 ≤ 𝑀 , 𝑀 , 𝑛 ) ) )
36	24 35	syld	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 [,) +∞ ) ) ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 < 𝑦 → 𝐵 ≤ if ( 𝑛 ≤ 𝑀 , 𝑀 , 𝑛 ) ) )
37	20 36	sylbird	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 [,) +∞ ) ) ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ¬ 𝑦 ≤ 𝑥 → 𝐵 ≤ if ( 𝑛 ≤ 𝑀 , 𝑀 , 𝑛 ) ) )
38		max1	⊢ ( ( 𝑛 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → 𝑛 ≤ if ( 𝑛 ≤ 𝑀 , 𝑀 , 𝑛 ) )
39	25 26 38	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 [,) +∞ ) ) ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝑛 ≤ if ( 𝑛 ≤ 𝑀 , 𝑀 , 𝑛 ) )
40		letr	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ if ( 𝑛 ≤ 𝑀 , 𝑀 , 𝑛 ) ∈ ℝ ) → ( ( 𝐵 ≤ 𝑛 ∧ 𝑛 ≤ if ( 𝑛 ≤ 𝑀 , 𝑀 , 𝑛 ) ) → 𝐵 ≤ if ( 𝑛 ≤ 𝑀 , 𝑀 , 𝑛 ) ) )
41	29 25 32 40	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 [,) +∞ ) ) ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐵 ≤ 𝑛 ∧ 𝑛 ≤ if ( 𝑛 ≤ 𝑀 , 𝑀 , 𝑛 ) ) → 𝐵 ≤ if ( 𝑛 ≤ 𝑀 , 𝑀 , 𝑛 ) ) )
42	39 41	mpan2d	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 [,) +∞ ) ) ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ≤ 𝑛 → 𝐵 ≤ if ( 𝑛 ≤ 𝑀 , 𝑀 , 𝑛 ) ) )
43	37 42	jad	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 [,) +∞ ) ) ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛 ) → 𝐵 ≤ if ( 𝑛 ≤ 𝑀 , 𝑀 , 𝑛 ) ) )
44	43	ralimdva	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 [,) +∞ ) ) ∧ 𝑛 ∈ ℝ ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛 ) → ∀ 𝑥 ∈ 𝐴 𝐵 ≤ if ( 𝑛 ≤ 𝑀 , 𝑀 , 𝑛 ) ) )
45	44	impr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 [,) +∞ ) ) ∧ ( 𝑛 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛 ) ) ) → ∀ 𝑥 ∈ 𝐴 𝐵 ≤ if ( 𝑛 ≤ 𝑀 , 𝑀 , 𝑛 ) )
46		brralrspcev	⊢ ( ( if ( 𝑛 ≤ 𝑀 , 𝑀 , 𝑛 ) ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ if ( 𝑛 ≤ 𝑀 , 𝑀 , 𝑛 ) ) → ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑚 )
47	15 45 46	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 [,) +∞ ) ) ∧ ( 𝑛 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛 ) ) ) → ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑚 )
48	47	expr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 [,) +∞ ) ) ∧ 𝑛 ∈ ℝ ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛 ) → ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑚 ) )
49	48	rexlimdva	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 [,) +∞ ) ) → ( ∃ 𝑛 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛 ) → ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑚 ) )
50	49	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 𝐶 [,) +∞ ) ∃ 𝑛 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑛 ) → ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑚 ) )
51	8 50	mpd	⊢ ( 𝜑 → ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑚 )