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) ) )