# Metamath Proof Explorer

## Theorem lo1le

Description: Transfer eventual upper boundedness from a larger function to a smaller function. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Hypotheses lo1le.1 ${⊢}{\phi }\to {M}\in ℝ$
lo1le.2 ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right)\in \le 𝑂\left(1\right)$
lo1le.3 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in {V}$
lo1le.4 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {C}\in ℝ$
lo1le.5 ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {M}\le {x}\right)\right)\to {C}\le {B}$
Assertion lo1le ${⊢}{\phi }\to \left({x}\in {A}⟼{C}\right)\in \le 𝑂\left(1\right)$

### Proof

Step Hyp Ref Expression
1 lo1le.1 ${⊢}{\phi }\to {M}\in ℝ$
2 lo1le.2 ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right)\in \le 𝑂\left(1\right)$
3 lo1le.3 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in {V}$
4 lo1le.4 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {C}\in ℝ$
5 lo1le.5 ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {M}\le {x}\right)\right)\to {C}\le {B}$
6 simpr ${⊢}\left({\phi }\wedge {y}\in ℝ\right)\to {y}\in ℝ$
7 1 adantr ${⊢}\left({\phi }\wedge {y}\in ℝ\right)\to {M}\in ℝ$
8 6 7 ifcld ${⊢}\left({\phi }\wedge {y}\in ℝ\right)\to if\left({M}\le {y},{y},{M}\right)\in ℝ$
9 1 ad2antrr ${⊢}\left(\left({\phi }\wedge {y}\in ℝ\right)\wedge \left({m}\in ℝ\wedge {x}\in {A}\right)\right)\to {M}\in ℝ$
10 simplr ${⊢}\left(\left({\phi }\wedge {y}\in ℝ\right)\wedge \left({m}\in ℝ\wedge {x}\in {A}\right)\right)\to {y}\in ℝ$
11 3 ralrimiva ${⊢}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {V}$
12 dmmptg ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {V}\to \mathrm{dom}\left({x}\in {A}⟼{B}\right)={A}$
13 11 12 syl ${⊢}{\phi }\to \mathrm{dom}\left({x}\in {A}⟼{B}\right)={A}$
14 lo1dm ${⊢}\left({x}\in {A}⟼{B}\right)\in \le 𝑂\left(1\right)\to \mathrm{dom}\left({x}\in {A}⟼{B}\right)\subseteq ℝ$
15 2 14 syl ${⊢}{\phi }\to \mathrm{dom}\left({x}\in {A}⟼{B}\right)\subseteq ℝ$
16 13 15 eqsstrrd ${⊢}{\phi }\to {A}\subseteq ℝ$
17 16 ad2antrr ${⊢}\left(\left({\phi }\wedge {y}\in ℝ\right)\wedge \left({m}\in ℝ\wedge {x}\in {A}\right)\right)\to {A}\subseteq ℝ$
18 simprr ${⊢}\left(\left({\phi }\wedge {y}\in ℝ\right)\wedge \left({m}\in ℝ\wedge {x}\in {A}\right)\right)\to {x}\in {A}$
19 17 18 sseldd ${⊢}\left(\left({\phi }\wedge {y}\in ℝ\right)\wedge \left({m}\in ℝ\wedge {x}\in {A}\right)\right)\to {x}\in ℝ$
20 maxle ${⊢}\left({M}\in ℝ\wedge {y}\in ℝ\wedge {x}\in ℝ\right)\to \left(if\left({M}\le {y},{y},{M}\right)\le {x}↔\left({M}\le {x}\wedge {y}\le {x}\right)\right)$
21 9 10 19 20 syl3anc ${⊢}\left(\left({\phi }\wedge {y}\in ℝ\right)\wedge \left({m}\in ℝ\wedge {x}\in {A}\right)\right)\to \left(if\left({M}\le {y},{y},{M}\right)\le {x}↔\left({M}\le {x}\wedge {y}\le {x}\right)\right)$
22 simpr ${⊢}\left({M}\le {x}\wedge {y}\le {x}\right)\to {y}\le {x}$
23 21 22 syl6bi ${⊢}\left(\left({\phi }\wedge {y}\in ℝ\right)\wedge \left({m}\in ℝ\wedge {x}\in {A}\right)\right)\to \left(if\left({M}\le {y},{y},{M}\right)\le {x}\to {y}\le {x}\right)$
24 23 imim1d ${⊢}\left(\left({\phi }\wedge {y}\in ℝ\right)\wedge \left({m}\in ℝ\wedge {x}\in {A}\right)\right)\to \left(\left({y}\le {x}\to {B}\le {m}\right)\to \left(if\left({M}\le {y},{y},{M}\right)\le {x}\to {B}\le {m}\right)\right)$
25 5 adantlr ${⊢}\left(\left({\phi }\wedge {y}\in ℝ\right)\wedge \left({x}\in {A}\wedge {M}\le {x}\right)\right)\to {C}\le {B}$
26 25 adantrll ${⊢}\left(\left({\phi }\wedge {y}\in ℝ\right)\wedge \left(\left({m}\in ℝ\wedge {x}\in {A}\right)\wedge {M}\le {x}\right)\right)\to {C}\le {B}$
27 simpl ${⊢}\left({\phi }\wedge {y}\in ℝ\right)\to {\phi }$
28 simplr ${⊢}\left(\left({m}\in ℝ\wedge {x}\in {A}\right)\wedge {M}\le {x}\right)\to {x}\in {A}$
29 27 28 4 syl2an ${⊢}\left(\left({\phi }\wedge {y}\in ℝ\right)\wedge \left(\left({m}\in ℝ\wedge {x}\in {A}\right)\wedge {M}\le {x}\right)\right)\to {C}\in ℝ$
30 3 2 lo1mptrcl ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in ℝ$
31 27 28 30 syl2an ${⊢}\left(\left({\phi }\wedge {y}\in ℝ\right)\wedge \left(\left({m}\in ℝ\wedge {x}\in {A}\right)\wedge {M}\le {x}\right)\right)\to {B}\in ℝ$
32 simprll ${⊢}\left(\left({\phi }\wedge {y}\in ℝ\right)\wedge \left(\left({m}\in ℝ\wedge {x}\in {A}\right)\wedge {M}\le {x}\right)\right)\to {m}\in ℝ$
33 letr ${⊢}\left({C}\in ℝ\wedge {B}\in ℝ\wedge {m}\in ℝ\right)\to \left(\left({C}\le {B}\wedge {B}\le {m}\right)\to {C}\le {m}\right)$
34 29 31 32 33 syl3anc ${⊢}\left(\left({\phi }\wedge {y}\in ℝ\right)\wedge \left(\left({m}\in ℝ\wedge {x}\in {A}\right)\wedge {M}\le {x}\right)\right)\to \left(\left({C}\le {B}\wedge {B}\le {m}\right)\to {C}\le {m}\right)$
35 26 34 mpand ${⊢}\left(\left({\phi }\wedge {y}\in ℝ\right)\wedge \left(\left({m}\in ℝ\wedge {x}\in {A}\right)\wedge {M}\le {x}\right)\right)\to \left({B}\le {m}\to {C}\le {m}\right)$
36 35 expr ${⊢}\left(\left({\phi }\wedge {y}\in ℝ\right)\wedge \left({m}\in ℝ\wedge {x}\in {A}\right)\right)\to \left({M}\le {x}\to \left({B}\le {m}\to {C}\le {m}\right)\right)$
37 36 adantrd ${⊢}\left(\left({\phi }\wedge {y}\in ℝ\right)\wedge \left({m}\in ℝ\wedge {x}\in {A}\right)\right)\to \left(\left({M}\le {x}\wedge {y}\le {x}\right)\to \left({B}\le {m}\to {C}\le {m}\right)\right)$
38 21 37 sylbid ${⊢}\left(\left({\phi }\wedge {y}\in ℝ\right)\wedge \left({m}\in ℝ\wedge {x}\in {A}\right)\right)\to \left(if\left({M}\le {y},{y},{M}\right)\le {x}\to \left({B}\le {m}\to {C}\le {m}\right)\right)$
39 38 a2d ${⊢}\left(\left({\phi }\wedge {y}\in ℝ\right)\wedge \left({m}\in ℝ\wedge {x}\in {A}\right)\right)\to \left(\left(if\left({M}\le {y},{y},{M}\right)\le {x}\to {B}\le {m}\right)\to \left(if\left({M}\le {y},{y},{M}\right)\le {x}\to {C}\le {m}\right)\right)$
40 24 39 syld ${⊢}\left(\left({\phi }\wedge {y}\in ℝ\right)\wedge \left({m}\in ℝ\wedge {x}\in {A}\right)\right)\to \left(\left({y}\le {x}\to {B}\le {m}\right)\to \left(if\left({M}\le {y},{y},{M}\right)\le {x}\to {C}\le {m}\right)\right)$
41 40 anassrs ${⊢}\left(\left(\left({\phi }\wedge {y}\in ℝ\right)\wedge {m}\in ℝ\right)\wedge {x}\in {A}\right)\to \left(\left({y}\le {x}\to {B}\le {m}\right)\to \left(if\left({M}\le {y},{y},{M}\right)\le {x}\to {C}\le {m}\right)\right)$
42 41 ralimdva ${⊢}\left(\left({\phi }\wedge {y}\in ℝ\right)\wedge {m}\in ℝ\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {m}\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(if\left({M}\le {y},{y},{M}\right)\le {x}\to {C}\le {m}\right)\right)$
43 42 reximdva ${⊢}\left({\phi }\wedge {y}\in ℝ\right)\to \left(\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {m}\right)\to \exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(if\left({M}\le {y},{y},{M}\right)\le {x}\to {C}\le {m}\right)\right)$
44 breq1 ${⊢}{z}=if\left({M}\le {y},{y},{M}\right)\to \left({z}\le {x}↔if\left({M}\le {y},{y},{M}\right)\le {x}\right)$
45 44 imbi1d ${⊢}{z}=if\left({M}\le {y},{y},{M}\right)\to \left(\left({z}\le {x}\to {C}\le {m}\right)↔\left(if\left({M}\le {y},{y},{M}\right)\le {x}\to {C}\le {m}\right)\right)$
46 45 rexralbidv ${⊢}{z}=if\left({M}\le {y},{y},{M}\right)\to \left(\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({z}\le {x}\to {C}\le {m}\right)↔\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(if\left({M}\le {y},{y},{M}\right)\le {x}\to {C}\le {m}\right)\right)$
47 46 rspcev ${⊢}\left(if\left({M}\le {y},{y},{M}\right)\in ℝ\wedge \exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(if\left({M}\le {y},{y},{M}\right)\le {x}\to {C}\le {m}\right)\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({z}\le {x}\to {C}\le {m}\right)$
48 8 43 47 syl6an ${⊢}\left({\phi }\wedge {y}\in ℝ\right)\to \left(\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {m}\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({z}\le {x}\to {C}\le {m}\right)\right)$
49 48 rexlimdva ${⊢}{\phi }\to \left(\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {m}\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({z}\le {x}\to {C}\le {m}\right)\right)$
50 16 30 ello1mpt ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right)\in \le 𝑂\left(1\right)↔\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\le {x}\to {B}\le {m}\right)\right)$
51 16 4 ello1mpt ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{C}\right)\in \le 𝑂\left(1\right)↔\exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {m}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({z}\le {x}\to {C}\le {m}\right)\right)$
52 49 50 51 3imtr4d ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right)\in \le 𝑂\left(1\right)\to \left({x}\in {A}⟼{C}\right)\in \le 𝑂\left(1\right)\right)$
53 2 52 mpd ${⊢}{\phi }\to \left({x}\in {A}⟼{C}\right)\in \le 𝑂\left(1\right)$