Metamath Proof Explorer

Theorem elbigoimp

Description: The defining property of a function of order G(x). (Contributed by AV, 18-May-2020)

Ref Expression
Assertion elbigoimp 
|- ( ( F e. ( _O ` G ) /\ F : A --> RR /\ A C_ dom G ) -> E. x e. RR E. m e. RR A. y e. A ( x <_ y -> ( F ` y ) <_ ( m x. ( G ` y ) ) ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( F e. ( _O ` G ) /\ F : A --> RR /\ A C_ dom G ) -> F e. ( _O ` G ) )
2 elbigofrcl 
 |-  ( F e. ( _O ` G ) -> G e. ( RR ^pm RR ) )
3 reex 
 |-  RR e. _V
4 3 3 elpm2 
 |-  ( G e. ( RR ^pm RR ) <-> ( G : dom G --> RR /\ dom G C_ RR ) )
5 2 4 sylib 
 |-  ( F e. ( _O ` G ) -> ( G : dom G --> RR /\ dom G C_ RR ) )
6 5 3ad2ant1 
 |-  ( ( F e. ( _O ` G ) /\ F : A --> RR /\ A C_ dom G ) -> ( G : dom G --> RR /\ dom G C_ RR ) )
7 3simpc 
 |-  ( ( F e. ( _O ` G ) /\ F : A --> RR /\ A C_ dom G ) -> ( F : A --> RR /\ A C_ dom G ) )
8 elbigo2 
 |-  ( ( ( G : dom G --> RR /\ dom G C_ RR ) /\ ( F : A --> RR /\ A C_ dom G ) ) -> ( F e. ( _O ` G ) <-> E. x e. RR E. m e. RR A. y e. A ( x <_ y -> ( F ` y ) <_ ( m x. ( G ` y ) ) ) ) )
9 6 7 8 syl2anc 
 |-  ( ( F e. ( _O ` G ) /\ F : A --> RR /\ A C_ dom G ) -> ( F e. ( _O ` G ) <-> E. x e. RR E. m e. RR A. y e. A ( x <_ y -> ( F ` y ) <_ ( m x. ( G ` y ) ) ) ) )
10 1 9 mpbid 
 |-  ( ( F e. ( _O ` G ) /\ F : A --> RR /\ A C_ dom G ) -> E. x e. RR E. m e. RR A. y e. A ( x <_ y -> ( F ` y ) <_ ( m x. ( G ` y ) ) ) )