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
|- ( ( ph /\ x e. A ) -> B e. RR )
lo1eq.2
|- ( ( ph /\ x e. A ) -> C e. RR )
lo1eq.3
|- ( ph -> D e. RR )
lo1eq.4
|- ( ( ph /\ ( x e. A /\ D <_ x ) ) -> B = C )
Assertion lo1eq
|- ( ph -> ( ( x e. A |-> B ) e. <_O(1) <-> ( x e. A |-> C ) e. <_O(1) ) )

Proof

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