Metamath Proof Explorer

Theorem elbigodm

Description: The domain of a function of order G(x) is a subset of the reals. (Contributed by AV, 18-May-2020)

Ref Expression
Assertion elbigodm 
|- ( F e. ( _O ` G ) -> dom F C_ 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 simprbi 
 |-  ( F e. ( RR ^pm RR ) -> dom F C_ 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 ) ) ) -> dom F C_ RR )
6 1 5 sylbi 
 |-  ( F e. ( _O ` G ) -> dom F C_ RR )