Metamath Proof Explorer

Theorem o1compt

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

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

Proof

Step Hyp Ref Expression
1 o1compt.1 
 |-  ( ph -> F : A --> CC )
2 o1compt.2 
 |-  ( ph -> F e. O(1) )
3 o1compt.3 
 |-  ( ( ph /\ y e. B ) -> C e. A )
4 o1compt.4 
 |-  ( ph -> B C_ RR )
5 o1compt.5 
 |-  ( ( ph /\ m e. RR ) -> E. x e. RR A. y e. B ( x <_ y -> m <_ C ) )
6 3 fmpttd 
 |-  ( ph -> ( y e. B |-> C ) : B --> A )
7 nfv 
 |-  F/ y x <_ z
8 nfcv 
 |-  F/_ y m
9 nfcv 
 |-  F/_ y <_
10 nffvmpt1 
 |-  F/_ y ( ( y e. B |-> C ) ` z )
11 8 9 10 nfbr 
 |-  F/ y m <_ ( ( y e. B |-> C ) ` z )
12 7 11 nfim 
 |-  F/ y ( x <_ z -> m <_ ( ( y e. B |-> C ) ` z ) )
13 nfv 
 |-  F/ z ( x <_ y -> m <_ ( ( y e. B |-> C ) ` y ) )
14 breq2 
 |-  ( z = y -> ( x <_ z <-> x <_ y ) )
15 fveq2 
 |-  ( z = y -> ( ( y e. B |-> C ) ` z ) = ( ( y e. B |-> C ) ` y ) )
16 15 breq2d 
 |-  ( z = y -> ( m <_ ( ( y e. B |-> C ) ` z ) <-> m <_ ( ( y e. B |-> C ) ` y ) ) )
17 14 16 imbi12d 
 |-  ( z = y -> ( ( x <_ z -> m <_ ( ( y e. B |-> C ) ` z ) ) <-> ( x <_ y -> m <_ ( ( y e. B |-> C ) ` y ) ) ) )
18 12 13 17 cbvralw 
 |-  ( A. z e. B ( x <_ z -> m <_ ( ( y e. B |-> C ) ` z ) ) <-> A. y e. B ( x <_ y -> m <_ ( ( y e. B |-> C ) ` y ) ) )
19 simpr 
 |-  ( ( ph /\ y e. B ) -> y e. B )
20 eqid 
 |-  ( y e. B |-> C ) = ( y e. B |-> C )
21 20 fvmpt2 
 |-  ( ( y e. B /\ C e. A ) -> ( ( y e. B |-> C ) ` y ) = C )
22 19 3 21 syl2anc 
 |-  ( ( ph /\ y e. B ) -> ( ( y e. B |-> C ) ` y ) = C )
23 22 breq2d 
 |-  ( ( ph /\ y e. B ) -> ( m <_ ( ( y e. B |-> C ) ` y ) <-> m <_ C ) )
24 23 imbi2d 
 |-  ( ( ph /\ y e. B ) -> ( ( x <_ y -> m <_ ( ( y e. B |-> C ) ` y ) ) <-> ( x <_ y -> m <_ C ) ) )
25 24 ralbidva 
 |-  ( ph -> ( A. y e. B ( x <_ y -> m <_ ( ( y e. B |-> C ) ` y ) ) <-> A. y e. B ( x <_ y -> m <_ C ) ) )
26 18 25 bitrid 
 |-  ( ph -> ( A. z e. B ( x <_ z -> m <_ ( ( y e. B |-> C ) ` z ) ) <-> A. y e. B ( x <_ y -> m <_ C ) ) )
27 26 rexbidv 
 |-  ( ph -> ( E. x e. RR A. z e. B ( x <_ z -> m <_ ( ( y e. B |-> C ) ` z ) ) <-> E. x e. RR A. y e. B ( x <_ y -> m <_ C ) ) )
28 27 adantr 
 |-  ( ( ph /\ m e. RR ) -> ( E. x e. RR A. z e. B ( x <_ z -> m <_ ( ( y e. B |-> C ) ` z ) ) <-> E. x e. RR A. y e. B ( x <_ y -> m <_ C ) ) )
29 5 28 mpbird 
 |-  ( ( ph /\ m e. RR ) -> E. x e. RR A. z e. B ( x <_ z -> m <_ ( ( y e. B |-> C ) ` z ) ) )
30 1 2 6 4 29 o1co 
 |-  ( ph -> ( F o. ( y e. B |-> C ) ) e. O(1) )