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