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 φ x A B
lo1eq.2 φ x A C
lo1eq.3 φ D
lo1eq.4 φ x A D x B = C
Assertion lo1eq φ x A B 𝑂1 x A C 𝑂1

Proof

Step Hyp Ref Expression
1 lo1eq.1 φ x A B
2 lo1eq.2 φ x A C
3 lo1eq.3 φ D
4 lo1eq.4 φ x A D x B = C
5 lo1dm x A B 𝑂1 dom x A B
6 eqid x A B = x A B
7 6 1 dmmptd φ dom x A B = A
8 7 sseq1d φ dom x A B A
9 5 8 syl5ib φ x A B 𝑂1 A
10 lo1dm x A C 𝑂1 dom x A C
11 eqid x A C = x A C
12 11 2 dmmptd φ dom x A C = A
13 12 sseq1d φ dom x A C A
14 10 13 syl5ib φ x A C 𝑂1 A
15 simpr φ x A D +∞ x A D +∞
16 elin x A D +∞ x A x D +∞
17 15 16 sylib φ x A D +∞ x A x D +∞
18 17 simpld φ x A D +∞ x A
19 17 simprd φ x A D +∞ x D +∞
20 elicopnf D x D +∞ x D x
21 3 20 syl φ x D +∞ x D x
22 21 biimpa φ x D +∞ x D x
23 19 22 syldan φ x A D +∞ x D x
24 23 simprd φ x A D +∞ D x
25 18 24 jca φ x A D +∞ x A D x
26 25 4 syldan φ x A D +∞ B = C
27 26 mpteq2dva φ x A D +∞ B = x A D +∞ C
28 inss1 A D +∞ A
29 resmpt A D +∞ A x A B A D +∞ = x A D +∞ B
30 28 29 ax-mp x A B A D +∞ = x A D +∞ B
31 resmpt A D +∞ A x A C A D +∞ = x A D +∞ C
32 28 31 ax-mp x A C A D +∞ = x A D +∞ C
33 27 30 32 3eqtr4g φ x A B A D +∞ = x A C A D +∞
34 resres x A B A D +∞ = x A B A D +∞
35 resres x A C A D +∞ = x A C A D +∞
36 33 34 35 3eqtr4g φ x A B A D +∞ = x A C A D +∞
37 ssid A A
38 resmpt A A x A B A = x A B
39 reseq1 x A B A = x A B x A B A D +∞ = x A B D +∞
40 37 38 39 mp2b x A B A D +∞ = x A B D +∞
41 resmpt A A x A C A = x A C
42 reseq1 x A C A = x A C x A C A D +∞ = x A C D +∞
43 37 41 42 mp2b x A C A D +∞ = x A C D +∞
44 36 40 43 3eqtr3g φ x A B D +∞ = x A C D +∞
45 44 eleq1d φ x A B D +∞ 𝑂1 x A C D +∞ 𝑂1
46 45 adantr φ A x A B D +∞ 𝑂1 x A C D +∞ 𝑂1
47 1 fmpttd φ x A B : A
48 47 adantr φ A x A B : A
49 simpr φ A A
50 3 adantr φ A D
51 48 49 50 lo1resb φ A x A B 𝑂1 x A B D +∞ 𝑂1
52 2 fmpttd φ x A C : A
53 52 adantr φ A x A C : A
54 53 49 50 lo1resb φ A x A C 𝑂1 x A C D +∞ 𝑂1
55 46 51 54 3bitr4d φ A x A B 𝑂1 x A C 𝑂1
56 55 ex φ A x A B 𝑂1 x A C 𝑂1
57 9 14 56 pm5.21ndd φ x A B 𝑂1 x A C 𝑂1