Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
lo1resb.2 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
lo1resb.3 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
Assertion lo1resb ( 𝜑 → ( 𝐹 ∈ ≤𝑂(1) ↔ ( 𝐹 ↾ ( 𝐵 [,) +∞ ) ) ∈ ≤𝑂(1) ) )

Proof

Step Hyp Ref Expression
1 lo1resb.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
2 lo1resb.2 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
3 lo1resb.3 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4 lo1res ⊢ ( 𝐹 ∈ ≤𝑂(1) → ( 𝐹 ↾ ( 𝐵 [,) +∞ ) ) ∈ ≤𝑂(1) )
5 1 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )
6 5 reseq1d ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐵 [,) +∞ ) ) = ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) ↾ ( 𝐵 [,) +∞ ) ) )
7 resmpt3 ⊢ ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) ↾ ( 𝐵 [,) +∞ ) ) = ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ↦ ( 𝐹 ‘ 𝑥 ) )
8 6 7 eqtrdi ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐵 [,) +∞ ) ) = ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ↦ ( 𝐹 ‘ 𝑥 ) ) )
9 8 eleq1d ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐵 [,) +∞ ) ) ∈ ≤𝑂(1) ↔ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ ≤𝑂(1) ) )
10 inss1 ⊢ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ⊆ 𝐴
11 10 2 sstrid ⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ⊆ ℝ )
12 elinel1 ⊢ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) → 𝑥 ∈ 𝐴 )
13 ffvelrn ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
14 1 12 13 syl2an ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
15 11 14 ello1mpt ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ ≤𝑂(1) ↔ ∃ 𝑦 ∈ ℝ ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ( 𝑦 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑧 ) ) )
16 elin ⊢ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐵 [,) +∞ ) ) )
17 16 imbi1i ⊢ ( ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) → ( 𝑦 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑧 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐵 [,) +∞ ) ) → ( 𝑦 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑧 ) ) )
18 impexp ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐵 [,) +∞ ) ) → ( 𝑦 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑧 ) ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ ( 𝐵 [,) +∞ ) → ( 𝑦 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑧 ) ) ) )
19 17 18 bitri ⊢ ( ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) → ( 𝑦 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑧 ) ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ ( 𝐵 [,) +∞ ) → ( 𝑦 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑧 ) ) ) )
20 impexp ⊢ ( ( ( 𝑥 ∈ ( 𝐵 [,) +∞ ) ∧ 𝑦 ≤ 𝑥 ) → ( 𝐹 ‘ 𝑥 ) ≤ 𝑧 ) ↔ ( 𝑥 ∈ ( 𝐵 [,) +∞ ) → ( 𝑦 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑧 ) ) )
21 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
22 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → 𝐴 ⊆ ℝ )
23 22 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
24 elicopnf ⊢ ( 𝐵 ∈ ℝ → ( 𝑥 ∈ ( 𝐵 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐵 ≤ 𝑥 ) ) )
25 24 baibd ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( 𝐵 [,) +∞ ) ↔ 𝐵 ≤ 𝑥 ) )
26 21 23 25 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ ( 𝐵 [,) +∞ ) ↔ 𝐵 ≤ 𝑥 ) )
27 26 anbi1d ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ ( 𝐵 [,) +∞ ) ∧ 𝑦 ≤ 𝑥 ) ↔ ( 𝐵 ≤ 𝑥 ∧ 𝑦 ≤ 𝑥 ) ) )
28 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ ℝ )
29 maxle ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( if ( 𝐵 ≤ 𝑦 , 𝑦 , 𝐵 ) ≤ 𝑥 ↔ ( 𝐵 ≤ 𝑥 ∧ 𝑦 ≤ 𝑥 ) ) )
30 21 28 23 29 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( if ( 𝐵 ≤ 𝑦 , 𝑦 , 𝐵 ) ≤ 𝑥 ↔ ( 𝐵 ≤ 𝑥 ∧ 𝑦 ≤ 𝑥 ) ) )
31 27 30 bitr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ ( 𝐵 [,) +∞ ) ∧ 𝑦 ≤ 𝑥 ) ↔ if ( 𝐵 ≤ 𝑦 , 𝑦 , 𝐵 ) ≤ 𝑥 ) )
32 31 imbi1d ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ ( 𝐵 [,) +∞ ) ∧ 𝑦 ≤ 𝑥 ) → ( 𝐹 ‘ 𝑥 ) ≤ 𝑧 ) ↔ ( if ( 𝐵 ≤ 𝑦 , 𝑦 , 𝐵 ) ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑧 ) ) )
33 20 32 bitr3id ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ ( 𝐵 [,) +∞ ) → ( 𝑦 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑧 ) ) ↔ ( if ( 𝐵 ≤ 𝑦 , 𝑦 , 𝐵 ) ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑧 ) ) )
34 33 pm5.74da ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ ( 𝐵 [,) +∞ ) → ( 𝑦 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑧 ) ) ) ↔ ( 𝑥 ∈ 𝐴 → ( if ( 𝐵 ≤ 𝑦 , 𝑦 , 𝐵 ) ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑧 ) ) ) )
35 19 34 syl5bb ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) → ( 𝑦 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑧 ) ) ↔ ( 𝑥 ∈ 𝐴 → ( if ( 𝐵 ≤ 𝑦 , 𝑦 , 𝐵 ) ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑧 ) ) ) )
36 35 ralbidv2 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( ∀ 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ( 𝑦 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑧 ) ↔ ∀ 𝑥 ∈ 𝐴 ( if ( 𝐵 ≤ 𝑦 , 𝑦 , 𝐵 ) ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑧 ) ) )
37 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → 𝐹 : 𝐴 ⟶ ℝ )
38 simprl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → 𝑦 ∈ ℝ )
39 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → 𝐵 ∈ ℝ )
40 38 39 ifcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → if ( 𝐵 ≤ 𝑦 , 𝑦 , 𝐵 ) ∈ ℝ )
41 simprr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → 𝑧 ∈ ℝ )
42 ello12r ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( if ( 𝐵 ≤ 𝑦 , 𝑦 , 𝐵 ) ∈ ℝ ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ( if ( 𝐵 ≤ 𝑦 , 𝑦 , 𝐵 ) ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑧 ) ) → 𝐹 ∈ ≤𝑂(1) )
43 42 3expia ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( if ( 𝐵 ≤ 𝑦 , 𝑦 , 𝐵 ) ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( ∀ 𝑥 ∈ 𝐴 ( if ( 𝐵 ≤ 𝑦 , 𝑦 , 𝐵 ) ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑧 ) → 𝐹 ∈ ≤𝑂(1) ) )
44 37 22 40 41 43 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( ∀ 𝑥 ∈ 𝐴 ( if ( 𝐵 ≤ 𝑦 , 𝑦 , 𝐵 ) ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑧 ) → 𝐹 ∈ ≤𝑂(1) ) )
45 36 44 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( ∀ 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ( 𝑦 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑧 ) → 𝐹 ∈ ≤𝑂(1) ) )
46 45 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ( 𝑦 ≤ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≤ 𝑧 ) → 𝐹 ∈ ≤𝑂(1) ) )
47 15 46 sylbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ ≤𝑂(1) → 𝐹 ∈ ≤𝑂(1) ) )
48 9 47 sylbid ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐵 [,) +∞ ) ) ∈ ≤𝑂(1) → 𝐹 ∈ ≤𝑂(1) ) )
49 4 48 impbid2 ⊢ ( 𝜑 → ( 𝐹 ∈ ≤𝑂(1) ↔ ( 𝐹 ↾ ( 𝐵 [,) +∞ ) ) ∈ ≤𝑂(1) ) )