Metamath Proof Explorer

Theorem o1co

Description: Sufficient condition for transforming the index set of an eventually bounded function. (Contributed by Mario Carneiro, 12-May-2016)

Ref Expression
Hypotheses o1co.1 
|- ( ph -> F : A --> CC )
o1co.2 
|- ( ph -> F e. O(1) )
o1co.3 
|- ( ph -> G : B --> A )
o1co.4 
|- ( ph -> B C_ RR )
o1co.5 
|- ( ( ph /\ m e. RR ) -> E. x e. RR A. y e. B ( x <_ y -> m <_ ( G ` y ) ) )
Assertion o1co 
|- ( ph -> ( F o. G ) e. O(1) )

Proof

Step Hyp Ref Expression
1 o1co.1 
 |-  ( ph -> F : A --> CC )
2 o1co.2 
 |-  ( ph -> F e. O(1) )
3 o1co.3 
 |-  ( ph -> G : B --> A )
4 o1co.4 
 |-  ( ph -> B C_ RR )
5 o1co.5 
 |-  ( ( ph /\ m e. RR ) -> E. x e. RR A. y e. B ( x <_ y -> m <_ ( G ` y ) ) )
6 1 fdmd 
 |-  ( ph -> dom F = A )
7 o1dm 
 |-  ( F e. O(1) -> dom F C_ RR )
8 2 7 syl 
 |-  ( ph -> dom F C_ RR )
9 6 8 eqsstrrd 
 |-  ( ph -> A C_ RR )
10 elo12 
 |-  ( ( F : A --> CC /\ A C_ RR ) -> ( F e. O(1) <-> E. m e. RR E. n e. RR A. z e. A ( m <_ z -> ( abs ` ( F ` z ) ) <_ n ) ) )
11 1 9 10 syl2anc 
 |-  ( ph -> ( F e. O(1) <-> E. m e. RR E. n e. RR A. z e. A ( m <_ z -> ( abs ` ( F ` z ) ) <_ n ) ) )
12 2 11 mpbid 
 |-  ( ph -> E. m e. RR E. n e. RR A. z e. A ( m <_ z -> ( abs ` ( F ` z ) ) <_ n ) )
13 reeanv 
 |-  ( E. x e. RR E. n e. RR ( A. y e. B ( x <_ y -> m <_ ( G ` y ) ) /\ A. z e. A ( m <_ z -> ( abs ` ( F ` z ) ) <_ n ) ) <-> ( E. x e. RR A. y e. B ( x <_ y -> m <_ ( G ` y ) ) /\ E. n e. RR A. z e. A ( m <_ z -> ( abs ` ( F ` z ) ) <_ n ) ) )
14 3 ad3antrrr 
 |-  ( ( ( ( ph /\ m e. RR ) /\ x e. RR ) /\ n e. RR ) -> G : B --> A )
15 14 ffvelrnda 
 |-  ( ( ( ( ( ph /\ m e. RR ) /\ x e. RR ) /\ n e. RR ) /\ y e. B ) -> ( G ` y ) e. A )
16 breq2 
 |-  ( z = ( G ` y ) -> ( m <_ z <-> m <_ ( G ` y ) ) )
17 2fveq3 
 |-  ( z = ( G ` y ) -> ( abs ` ( F ` z ) ) = ( abs ` ( F ` ( G ` y ) ) ) )
18 17 breq1d 
 |-  ( z = ( G ` y ) -> ( ( abs ` ( F ` z ) ) <_ n <-> ( abs ` ( F ` ( G ` y ) ) ) <_ n ) )
19 16 18 imbi12d 
 |-  ( z = ( G ` y ) -> ( ( m <_ z -> ( abs ` ( F ` z ) ) <_ n ) <-> ( m <_ ( G ` y ) -> ( abs ` ( F ` ( G ` y ) ) ) <_ n ) ) )
20 19 rspcva 
 |-  ( ( ( G ` y ) e. A /\ A. z e. A ( m <_ z -> ( abs ` ( F ` z ) ) <_ n ) ) -> ( m <_ ( G ` y ) -> ( abs ` ( F ` ( G ` y ) ) ) <_ n ) )
21 15 20 sylan 
 |-  ( ( ( ( ( ( ph /\ m e. RR ) /\ x e. RR ) /\ n e. RR ) /\ y e. B ) /\ A. z e. A ( m <_ z -> ( abs ` ( F ` z ) ) <_ n ) ) -> ( m <_ ( G ` y ) -> ( abs ` ( F ` ( G ` y ) ) ) <_ n ) )
22 21 an32s 
 |-  ( ( ( ( ( ( ph /\ m e. RR ) /\ x e. RR ) /\ n e. RR ) /\ A. z e. A ( m <_ z -> ( abs ` ( F ` z ) ) <_ n ) ) /\ y e. B ) -> ( m <_ ( G ` y ) -> ( abs ` ( F ` ( G ` y ) ) ) <_ n ) )
23 14 adantr 
 |-  ( ( ( ( ( ph /\ m e. RR ) /\ x e. RR ) /\ n e. RR ) /\ A. z e. A ( m <_ z -> ( abs ` ( F ` z ) ) <_ n ) ) -> G : B --> A )
24 fvco3 
 |-  ( ( G : B --> A /\ y e. B ) -> ( ( F o. G ) ` y ) = ( F ` ( G ` y ) ) )
25 23 24 sylan 
 |-  ( ( ( ( ( ( ph /\ m e. RR ) /\ x e. RR ) /\ n e. RR ) /\ A. z e. A ( m <_ z -> ( abs ` ( F ` z ) ) <_ n ) ) /\ y e. B ) -> ( ( F o. G ) ` y ) = ( F ` ( G ` y ) ) )
26 25 fveq2d 
 |-  ( ( ( ( ( ( ph /\ m e. RR ) /\ x e. RR ) /\ n e. RR ) /\ A. z e. A ( m <_ z -> ( abs ` ( F ` z ) ) <_ n ) ) /\ y e. B ) -> ( abs ` ( ( F o. G ) ` y ) ) = ( abs ` ( F ` ( G ` y ) ) ) )
27 26 breq1d 
 |-  ( ( ( ( ( ( ph /\ m e. RR ) /\ x e. RR ) /\ n e. RR ) /\ A. z e. A ( m <_ z -> ( abs ` ( F ` z ) ) <_ n ) ) /\ y e. B ) -> ( ( abs ` ( ( F o. G ) ` y ) ) <_ n <-> ( abs ` ( F ` ( G ` y ) ) ) <_ n ) )
28 22 27 sylibrd 
 |-  ( ( ( ( ( ( ph /\ m e. RR ) /\ x e. RR ) /\ n e. RR ) /\ A. z e. A ( m <_ z -> ( abs ` ( F ` z ) ) <_ n ) ) /\ y e. B ) -> ( m <_ ( G ` y ) -> ( abs ` ( ( F o. G ) ` y ) ) <_ n ) )
29 28 imim2d 
 |-  ( ( ( ( ( ( ph /\ m e. RR ) /\ x e. RR ) /\ n e. RR ) /\ A. z e. A ( m <_ z -> ( abs ` ( F ` z ) ) <_ n ) ) /\ y e. B ) -> ( ( x <_ y -> m <_ ( G ` y ) ) -> ( x <_ y -> ( abs ` ( ( F o. G ) ` y ) ) <_ n ) ) )
30 29 ralimdva 
 |-  ( ( ( ( ( ph /\ m e. RR ) /\ x e. RR ) /\ n e. RR ) /\ A. z e. A ( m <_ z -> ( abs ` ( F ` z ) ) <_ n ) ) -> ( A. y e. B ( x <_ y -> m <_ ( G ` y ) ) -> A. y e. B ( x <_ y -> ( abs ` ( ( F o. G ) ` y ) ) <_ n ) ) )
31 30 expimpd 
 |-  ( ( ( ( ph /\ m e. RR ) /\ x e. RR ) /\ n e. RR ) -> ( ( A. z e. A ( m <_ z -> ( abs ` ( F ` z ) ) <_ n ) /\ A. y e. B ( x <_ y -> m <_ ( G ` y ) ) ) -> A. y e. B ( x <_ y -> ( abs ` ( ( F o. G ) ` y ) ) <_ n ) ) )
32 31 ancomsd 
 |-  ( ( ( ( ph /\ m e. RR ) /\ x e. RR ) /\ n e. RR ) -> ( ( A. y e. B ( x <_ y -> m <_ ( G ` y ) ) /\ A. z e. A ( m <_ z -> ( abs ` ( F ` z ) ) <_ n ) ) -> A. y e. B ( x <_ y -> ( abs ` ( ( F o. G ) ` y ) ) <_ n ) ) )
33 32 reximdva 
 |-  ( ( ( ph /\ m e. RR ) /\ x e. RR ) -> ( E. n e. RR ( A. y e. B ( x <_ y -> m <_ ( G ` y ) ) /\ A. z e. A ( m <_ z -> ( abs ` ( F ` z ) ) <_ n ) ) -> E. n e. RR A. y e. B ( x <_ y -> ( abs ` ( ( F o. G ) ` y ) ) <_ n ) ) )
34 33 reximdva 
 |-  ( ( ph /\ m e. RR ) -> ( E. x e. RR E. n e. RR ( A. y e. B ( x <_ y -> m <_ ( G ` y ) ) /\ A. z e. A ( m <_ z -> ( abs ` ( F ` z ) ) <_ n ) ) -> E. x e. RR E. n e. RR A. y e. B ( x <_ y -> ( abs ` ( ( F o. G ) ` y ) ) <_ n ) ) )
35 13 34 syl5bir 
 |-  ( ( ph /\ m e. RR ) -> ( ( E. x e. RR A. y e. B ( x <_ y -> m <_ ( G ` y ) ) /\ E. n e. RR A. z e. A ( m <_ z -> ( abs ` ( F ` z ) ) <_ n ) ) -> E. x e. RR E. n e. RR A. y e. B ( x <_ y -> ( abs ` ( ( F o. G ) ` y ) ) <_ n ) ) )
36 5 35 mpand 
 |-  ( ( ph /\ m e. RR ) -> ( E. n e. RR A. z e. A ( m <_ z -> ( abs ` ( F ` z ) ) <_ n ) -> E. x e. RR E. n e. RR A. y e. B ( x <_ y -> ( abs ` ( ( F o. G ) ` y ) ) <_ n ) ) )
37 36 rexlimdva 
 |-  ( ph -> ( E. m e. RR E. n e. RR A. z e. A ( m <_ z -> ( abs ` ( F ` z ) ) <_ n ) -> E. x e. RR E. n e. RR A. y e. B ( x <_ y -> ( abs ` ( ( F o. G ) ` y ) ) <_ n ) ) )
38 12 37 mpd 
 |-  ( ph -> E. x e. RR E. n e. RR A. y e. B ( x <_ y -> ( abs ` ( ( F o. G ) ` y ) ) <_ n ) )
39 fco 
 |-  ( ( F : A --> CC /\ G : B --> A ) -> ( F o. G ) : B --> CC )
40 1 3 39 syl2anc 
 |-  ( ph -> ( F o. G ) : B --> CC )
41 elo12 
 |-  ( ( ( F o. G ) : B --> CC /\ B C_ RR ) -> ( ( F o. G ) e. O(1) <-> E. x e. RR E. n e. RR A. y e. B ( x <_ y -> ( abs ` ( ( F o. G ) ` y ) ) <_ n ) ) )
42 40 4 41 syl2anc 
 |-  ( ph -> ( ( F o. G ) e. O(1) <-> E. x e. RR E. n e. RR A. y e. B ( x <_ y -> ( abs ` ( ( F o. G ) ` y ) ) <_ n ) ) )
43 38 42 mpbird 
 |-  ( ph -> ( F o. G ) e. O(1) )