| Step |
Hyp |
Ref |
Expression |
| 1 |
|
fveq1 |
|- ( g = G -> ( g ` y ) = ( G ` y ) ) |
| 2 |
1
|
oveq2d |
|- ( g = G -> ( m x. ( g ` y ) ) = ( m x. ( G ` y ) ) ) |
| 3 |
2
|
breq2d |
|- ( g = G -> ( ( f ` y ) <_ ( m x. ( g ` y ) ) <-> ( f ` y ) <_ ( m x. ( G ` y ) ) ) ) |
| 4 |
3
|
ralbidv |
|- ( g = G -> ( A. y e. ( dom f i^i ( x [,) +oo ) ) ( f ` y ) <_ ( m x. ( g ` y ) ) <-> A. y e. ( dom f i^i ( x [,) +oo ) ) ( f ` y ) <_ ( m x. ( G ` y ) ) ) ) |
| 5 |
4
|
2rexbidv |
|- ( g = G -> ( E. x e. RR E. m e. RR A. y e. ( dom f i^i ( x [,) +oo ) ) ( f ` y ) <_ ( m x. ( g ` y ) ) <-> E. x e. RR E. m e. RR A. y e. ( dom f i^i ( x [,) +oo ) ) ( f ` y ) <_ ( m x. ( G ` y ) ) ) ) |
| 6 |
5
|
rabbidv |
|- ( g = G -> { 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 ) ) } = { 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 ) ) } ) |
| 7 |
|
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 ) ) } ) |
| 8 |
|
ovex |
|- ( RR ^pm RR ) e. _V |
| 9 |
8
|
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 |
| 10 |
6 7 9
|
fvmpt |
|- ( G e. ( RR ^pm RR ) -> ( _O ` G ) = { 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 ) ) } ) |