# Metamath Proof Explorer

## Theorem lo1eq

Description: Two functions that are eventually equal to one another are eventually bounded if one of them is. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Hypotheses lo1eq.1 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in ℝ$
lo1eq.2 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {C}\in ℝ$
lo1eq.3 ${⊢}{\phi }\to {D}\in ℝ$
lo1eq.4 ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {D}\le {x}\right)\right)\to {B}={C}$
Assertion lo1eq ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right)\in \le 𝑂\left(1\right)↔\left({x}\in {A}⟼{C}\right)\in \le 𝑂\left(1\right)\right)$

### Proof

Step Hyp Ref Expression
1 lo1eq.1 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in ℝ$
2 lo1eq.2 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {C}\in ℝ$
3 lo1eq.3 ${⊢}{\phi }\to {D}\in ℝ$
4 lo1eq.4 ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {D}\le {x}\right)\right)\to {B}={C}$
5 lo1dm ${⊢}\left({x}\in {A}⟼{B}\right)\in \le 𝑂\left(1\right)\to \mathrm{dom}\left({x}\in {A}⟼{B}\right)\subseteq ℝ$
6 eqid ${⊢}\left({x}\in {A}⟼{B}\right)=\left({x}\in {A}⟼{B}\right)$
7 6 1 dmmptd ${⊢}{\phi }\to \mathrm{dom}\left({x}\in {A}⟼{B}\right)={A}$
8 7 sseq1d ${⊢}{\phi }\to \left(\mathrm{dom}\left({x}\in {A}⟼{B}\right)\subseteq ℝ↔{A}\subseteq ℝ\right)$
9 5 8 syl5ib ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right)\in \le 𝑂\left(1\right)\to {A}\subseteq ℝ\right)$
10 lo1dm ${⊢}\left({x}\in {A}⟼{C}\right)\in \le 𝑂\left(1\right)\to \mathrm{dom}\left({x}\in {A}⟼{C}\right)\subseteq ℝ$
11 eqid ${⊢}\left({x}\in {A}⟼{C}\right)=\left({x}\in {A}⟼{C}\right)$
12 11 2 dmmptd ${⊢}{\phi }\to \mathrm{dom}\left({x}\in {A}⟼{C}\right)={A}$
13 12 sseq1d ${⊢}{\phi }\to \left(\mathrm{dom}\left({x}\in {A}⟼{C}\right)\subseteq ℝ↔{A}\subseteq ℝ\right)$
14 10 13 syl5ib ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{C}\right)\in \le 𝑂\left(1\right)\to {A}\subseteq ℝ\right)$
15 simpr ${⊢}\left({\phi }\wedge {x}\in \left({A}\cap \left[{D},\mathrm{+\infty }\right)\right)\right)\to {x}\in \left({A}\cap \left[{D},\mathrm{+\infty }\right)\right)$
16 elin ${⊢}{x}\in \left({A}\cap \left[{D},\mathrm{+\infty }\right)\right)↔\left({x}\in {A}\wedge {x}\in \left[{D},\mathrm{+\infty }\right)\right)$
17 15 16 sylib ${⊢}\left({\phi }\wedge {x}\in \left({A}\cap \left[{D},\mathrm{+\infty }\right)\right)\right)\to \left({x}\in {A}\wedge {x}\in \left[{D},\mathrm{+\infty }\right)\right)$
18 17 simpld ${⊢}\left({\phi }\wedge {x}\in \left({A}\cap \left[{D},\mathrm{+\infty }\right)\right)\right)\to {x}\in {A}$
19 17 simprd ${⊢}\left({\phi }\wedge {x}\in \left({A}\cap \left[{D},\mathrm{+\infty }\right)\right)\right)\to {x}\in \left[{D},\mathrm{+\infty }\right)$
20 elicopnf ${⊢}{D}\in ℝ\to \left({x}\in \left[{D},\mathrm{+\infty }\right)↔\left({x}\in ℝ\wedge {D}\le {x}\right)\right)$
21 3 20 syl ${⊢}{\phi }\to \left({x}\in \left[{D},\mathrm{+\infty }\right)↔\left({x}\in ℝ\wedge {D}\le {x}\right)\right)$
22 21 biimpa ${⊢}\left({\phi }\wedge {x}\in \left[{D},\mathrm{+\infty }\right)\right)\to \left({x}\in ℝ\wedge {D}\le {x}\right)$
23 19 22 syldan ${⊢}\left({\phi }\wedge {x}\in \left({A}\cap \left[{D},\mathrm{+\infty }\right)\right)\right)\to \left({x}\in ℝ\wedge {D}\le {x}\right)$
24 23 simprd ${⊢}\left({\phi }\wedge {x}\in \left({A}\cap \left[{D},\mathrm{+\infty }\right)\right)\right)\to {D}\le {x}$
25 18 24 jca ${⊢}\left({\phi }\wedge {x}\in \left({A}\cap \left[{D},\mathrm{+\infty }\right)\right)\right)\to \left({x}\in {A}\wedge {D}\le {x}\right)$
26 25 4 syldan ${⊢}\left({\phi }\wedge {x}\in \left({A}\cap \left[{D},\mathrm{+\infty }\right)\right)\right)\to {B}={C}$
27 26 mpteq2dva ${⊢}{\phi }\to \left({x}\in \left({A}\cap \left[{D},\mathrm{+\infty }\right)\right)⟼{B}\right)=\left({x}\in \left({A}\cap \left[{D},\mathrm{+\infty }\right)\right)⟼{C}\right)$
28 inss1 ${⊢}{A}\cap \left[{D},\mathrm{+\infty }\right)\subseteq {A}$
29 resmpt ${⊢}{A}\cap \left[{D},\mathrm{+\infty }\right)\subseteq {A}\to {\left({x}\in {A}⟼{B}\right)↾}_{\left({A}\cap \left[{D},\mathrm{+\infty }\right)\right)}=\left({x}\in \left({A}\cap \left[{D},\mathrm{+\infty }\right)\right)⟼{B}\right)$
30 28 29 ax-mp ${⊢}{\left({x}\in {A}⟼{B}\right)↾}_{\left({A}\cap \left[{D},\mathrm{+\infty }\right)\right)}=\left({x}\in \left({A}\cap \left[{D},\mathrm{+\infty }\right)\right)⟼{B}\right)$
31 resmpt ${⊢}{A}\cap \left[{D},\mathrm{+\infty }\right)\subseteq {A}\to {\left({x}\in {A}⟼{C}\right)↾}_{\left({A}\cap \left[{D},\mathrm{+\infty }\right)\right)}=\left({x}\in \left({A}\cap \left[{D},\mathrm{+\infty }\right)\right)⟼{C}\right)$
32 28 31 ax-mp ${⊢}{\left({x}\in {A}⟼{C}\right)↾}_{\left({A}\cap \left[{D},\mathrm{+\infty }\right)\right)}=\left({x}\in \left({A}\cap \left[{D},\mathrm{+\infty }\right)\right)⟼{C}\right)$
33 27 30 32 3eqtr4g ${⊢}{\phi }\to {\left({x}\in {A}⟼{B}\right)↾}_{\left({A}\cap \left[{D},\mathrm{+\infty }\right)\right)}={\left({x}\in {A}⟼{C}\right)↾}_{\left({A}\cap \left[{D},\mathrm{+\infty }\right)\right)}$
34 resres ${⊢}{\left({\left({x}\in {A}⟼{B}\right)↾}_{{A}}\right)↾}_{\left[{D},\mathrm{+\infty }\right)}={\left({x}\in {A}⟼{B}\right)↾}_{\left({A}\cap \left[{D},\mathrm{+\infty }\right)\right)}$
35 resres ${⊢}{\left({\left({x}\in {A}⟼{C}\right)↾}_{{A}}\right)↾}_{\left[{D},\mathrm{+\infty }\right)}={\left({x}\in {A}⟼{C}\right)↾}_{\left({A}\cap \left[{D},\mathrm{+\infty }\right)\right)}$
36 33 34 35 3eqtr4g ${⊢}{\phi }\to {\left({\left({x}\in {A}⟼{B}\right)↾}_{{A}}\right)↾}_{\left[{D},\mathrm{+\infty }\right)}={\left({\left({x}\in {A}⟼{C}\right)↾}_{{A}}\right)↾}_{\left[{D},\mathrm{+\infty }\right)}$
37 ssid ${⊢}{A}\subseteq {A}$
38 resmpt ${⊢}{A}\subseteq {A}\to {\left({x}\in {A}⟼{B}\right)↾}_{{A}}=\left({x}\in {A}⟼{B}\right)$
39 reseq1 ${⊢}{\left({x}\in {A}⟼{B}\right)↾}_{{A}}=\left({x}\in {A}⟼{B}\right)\to {\left({\left({x}\in {A}⟼{B}\right)↾}_{{A}}\right)↾}_{\left[{D},\mathrm{+\infty }\right)}={\left({x}\in {A}⟼{B}\right)↾}_{\left[{D},\mathrm{+\infty }\right)}$
40 37 38 39 mp2b ${⊢}{\left({\left({x}\in {A}⟼{B}\right)↾}_{{A}}\right)↾}_{\left[{D},\mathrm{+\infty }\right)}={\left({x}\in {A}⟼{B}\right)↾}_{\left[{D},\mathrm{+\infty }\right)}$
41 resmpt ${⊢}{A}\subseteq {A}\to {\left({x}\in {A}⟼{C}\right)↾}_{{A}}=\left({x}\in {A}⟼{C}\right)$
42 reseq1 ${⊢}{\left({x}\in {A}⟼{C}\right)↾}_{{A}}=\left({x}\in {A}⟼{C}\right)\to {\left({\left({x}\in {A}⟼{C}\right)↾}_{{A}}\right)↾}_{\left[{D},\mathrm{+\infty }\right)}={\left({x}\in {A}⟼{C}\right)↾}_{\left[{D},\mathrm{+\infty }\right)}$
43 37 41 42 mp2b ${⊢}{\left({\left({x}\in {A}⟼{C}\right)↾}_{{A}}\right)↾}_{\left[{D},\mathrm{+\infty }\right)}={\left({x}\in {A}⟼{C}\right)↾}_{\left[{D},\mathrm{+\infty }\right)}$
44 36 40 43 3eqtr3g ${⊢}{\phi }\to {\left({x}\in {A}⟼{B}\right)↾}_{\left[{D},\mathrm{+\infty }\right)}={\left({x}\in {A}⟼{C}\right)↾}_{\left[{D},\mathrm{+\infty }\right)}$
45 44 eleq1d ${⊢}{\phi }\to \left({\left({x}\in {A}⟼{B}\right)↾}_{\left[{D},\mathrm{+\infty }\right)}\in \le 𝑂\left(1\right)↔{\left({x}\in {A}⟼{C}\right)↾}_{\left[{D},\mathrm{+\infty }\right)}\in \le 𝑂\left(1\right)\right)$
46 45 adantr ${⊢}\left({\phi }\wedge {A}\subseteq ℝ\right)\to \left({\left({x}\in {A}⟼{B}\right)↾}_{\left[{D},\mathrm{+\infty }\right)}\in \le 𝑂\left(1\right)↔{\left({x}\in {A}⟼{C}\right)↾}_{\left[{D},\mathrm{+\infty }\right)}\in \le 𝑂\left(1\right)\right)$
47 1 fmpttd ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right):{A}⟶ℝ$
48 47 adantr ${⊢}\left({\phi }\wedge {A}\subseteq ℝ\right)\to \left({x}\in {A}⟼{B}\right):{A}⟶ℝ$
49 simpr ${⊢}\left({\phi }\wedge {A}\subseteq ℝ\right)\to {A}\subseteq ℝ$
50 3 adantr ${⊢}\left({\phi }\wedge {A}\subseteq ℝ\right)\to {D}\in ℝ$
51 48 49 50 lo1resb ${⊢}\left({\phi }\wedge {A}\subseteq ℝ\right)\to \left(\left({x}\in {A}⟼{B}\right)\in \le 𝑂\left(1\right)↔{\left({x}\in {A}⟼{B}\right)↾}_{\left[{D},\mathrm{+\infty }\right)}\in \le 𝑂\left(1\right)\right)$
52 2 fmpttd ${⊢}{\phi }\to \left({x}\in {A}⟼{C}\right):{A}⟶ℝ$
53 52 adantr ${⊢}\left({\phi }\wedge {A}\subseteq ℝ\right)\to \left({x}\in {A}⟼{C}\right):{A}⟶ℝ$
54 53 49 50 lo1resb ${⊢}\left({\phi }\wedge {A}\subseteq ℝ\right)\to \left(\left({x}\in {A}⟼{C}\right)\in \le 𝑂\left(1\right)↔{\left({x}\in {A}⟼{C}\right)↾}_{\left[{D},\mathrm{+\infty }\right)}\in \le 𝑂\left(1\right)\right)$
55 46 51 54 3bitr4d ${⊢}\left({\phi }\wedge {A}\subseteq ℝ\right)\to \left(\left({x}\in {A}⟼{B}\right)\in \le 𝑂\left(1\right)↔\left({x}\in {A}⟼{C}\right)\in \le 𝑂\left(1\right)\right)$
56 55 ex ${⊢}{\phi }\to \left({A}\subseteq ℝ\to \left(\left({x}\in {A}⟼{B}\right)\in \le 𝑂\left(1\right)↔\left({x}\in {A}⟼{C}\right)\in \le 𝑂\left(1\right)\right)\right)$
57 9 14 56 pm5.21ndd ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right)\in \le 𝑂\left(1\right)↔\left({x}\in {A}⟼{C}\right)\in \le 𝑂\left(1\right)\right)$