Metamath Proof Explorer

Theorem elbigof

Description: A function of order G(x) is a function. (Contributed by AV, 18-May-2020)

Ref Expression
Assertion elbigof 
|- ( F e. ( _O ` G ) -> F : dom F --> RR )

Proof

Step Hyp Ref Expression
1 elbigo 
 |-  ( F e. ( _O ` G ) <-> ( F e. ( RR ^pm RR ) /\ G e. ( RR ^pm RR ) /\ E. x e. RR E. m e. RR A. y e. ( dom F i^i ( x [,) +oo ) ) ( F ` y ) <_ ( m x. ( G ` y ) ) ) )
2 reex 
 |-  RR e. _V
3 2 2 elpm2 
 |-  ( F e. ( RR ^pm RR ) <-> ( F : dom F --> RR /\ dom F C_ RR ) )
4 3 simplbi 
 |-  ( F e. ( RR ^pm RR ) -> F : dom F --> RR )
5 4 3ad2ant1 
 |-  ( ( F e. ( RR ^pm RR ) /\ G e. ( RR ^pm RR ) /\ E. x e. RR E. m e. RR A. y e. ( dom F i^i ( x [,) +oo ) ) ( F ` y ) <_ ( m x. ( G ` y ) ) ) -> F : dom F --> RR )
6 1 5 sylbi 
 |-  ( F e. ( _O ` G ) -> F : dom F --> RR )