# 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 ${⊢}{\phi }\to {F}:{A}⟶ℝ$
lo1resb.2 ${⊢}{\phi }\to {A}\subseteq ℝ$
lo1resb.3 ${⊢}{\phi }\to {B}\in ℝ$
Assertion lo1resb ${⊢}{\phi }\to \left({F}\in \le 𝑂\left(1\right)↔{{F}↾}_{\left[{B},\mathrm{+\infty }\right)}\in \le 𝑂\left(1\right)\right)$

### Proof

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