Metamath Proof Explorer

Theorem elbigo2r

Description: Sufficient condition for a function to be of order G(x). (Contributed by AV, 18-May-2020)

Ref Expression
Assertion elbigo2r 
|- ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) /\ ( C e. RR /\ M e. RR /\ A. x e. B ( C <_ x -> ( F ` x ) <_ ( M x. ( G ` x ) ) ) ) ) -> F e. ( _O ` G ) )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( y = C -> ( y <_ x <-> C <_ x ) )
2 1 imbi1d 
 |-  ( y = C -> ( ( y <_ x -> ( F ` x ) <_ ( m x. ( G ` x ) ) ) <-> ( C <_ x -> ( F ` x ) <_ ( m x. ( G ` x ) ) ) ) )
3 2 ralbidv 
 |-  ( y = C -> ( A. x e. B ( y <_ x -> ( F ` x ) <_ ( m x. ( G ` x ) ) ) <-> A. x e. B ( C <_ x -> ( F ` x ) <_ ( m x. ( G ` x ) ) ) ) )
4 oveq1 
 |-  ( m = M -> ( m x. ( G ` x ) ) = ( M x. ( G ` x ) ) )
5 4 breq2d 
 |-  ( m = M -> ( ( F ` x ) <_ ( m x. ( G ` x ) ) <-> ( F ` x ) <_ ( M x. ( G ` x ) ) ) )
6 5 imbi2d 
 |-  ( m = M -> ( ( C <_ x -> ( F ` x ) <_ ( m x. ( G ` x ) ) ) <-> ( C <_ x -> ( F ` x ) <_ ( M x. ( G ` x ) ) ) ) )
7 6 ralbidv 
 |-  ( m = M -> ( A. x e. B ( C <_ x -> ( F ` x ) <_ ( m x. ( G ` x ) ) ) <-> A. x e. B ( C <_ x -> ( F ` x ) <_ ( M x. ( G ` x ) ) ) ) )
8 3 7 rspc2ev 
 |-  ( ( C e. RR /\ M e. RR /\ A. x e. B ( C <_ x -> ( F ` x ) <_ ( M x. ( G ` x ) ) ) ) -> E. y e. RR E. m e. RR A. x e. B ( y <_ x -> ( F ` x ) <_ ( m x. ( G ` x ) ) ) )
9 8 3ad2ant3 
 |-  ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) /\ ( C e. RR /\ M e. RR /\ A. x e. B ( C <_ x -> ( F ` x ) <_ ( M x. ( G ` x ) ) ) ) ) -> E. y e. RR E. m e. RR A. x e. B ( y <_ x -> ( F ` x ) <_ ( m x. ( G ` x ) ) ) )
10 elbigo2 
 |-  ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) ) -> ( F e. ( _O ` G ) <-> E. y e. RR E. m e. RR A. x e. B ( y <_ x -> ( F ` x ) <_ ( m x. ( G ` x ) ) ) ) )
11 10 3adant3 
 |-  ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) /\ ( C e. RR /\ M e. RR /\ A. x e. B ( C <_ x -> ( F ` x ) <_ ( M x. ( G ` x ) ) ) ) ) -> ( F e. ( _O ` G ) <-> E. y e. RR E. m e. RR A. x e. B ( y <_ x -> ( F ` x ) <_ ( m x. ( G ` x ) ) ) ) )
12 9 11 mpbird 
 |-  ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) /\ ( C e. RR /\ M e. RR /\ A. x e. B ( C <_ x -> ( F ` x ) <_ ( M x. ( G ` x ) ) ) ) ) -> F e. ( _O ` G ) )