Metamath Proof Explorer

Theorem elbigofrcl

Description: Reverse closure of the "big-O" function. (Contributed by AV, 16-May-2020)

Ref Expression
Assertion elbigofrcl 
|- ( F e. ( _O ` G ) -> G e. ( RR ^pm RR ) )

Proof

Step Hyp Ref Expression
1 elfvdm 
 |-  ( F e. ( _O ` G ) -> G e. dom _O )
2 df-bigo 
 |-  _O = ( g e. ( RR ^pm RR ) |-> { f 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 ) ) } )
3 2 dmeqi 
 |-  dom _O = dom ( g e. ( RR ^pm RR ) |-> { f 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 ) ) } )
4 dmmptg 
 |-  ( A. g e. ( RR ^pm RR ) { f 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 ) ) } e. _V -> dom ( g e. ( RR ^pm RR ) |-> { f 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 ) ) } ) = ( RR ^pm RR ) )
5 ovex 
 |-  ( RR ^pm RR ) e. _V
6 5 rabex 
 |-  { f 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 ) ) } e. _V
7 6 a1i 
 |-  ( g e. ( RR ^pm RR ) -> { f 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 ) ) } e. _V )
8 4 7 mprg 
 |-  dom ( g e. ( RR ^pm RR ) |-> { f 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 ) ) } ) = ( RR ^pm RR )
9 3 8 eqtri 
 |-  dom _O = ( RR ^pm RR )
10 1 9 eleqtrdi 
 |-  ( F e. ( _O ` G ) -> G e. ( RR ^pm RR ) )