Step |
Hyp |
Ref |
Expression |
1 |
|
bigoval |
|- ( 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 ) ) } ) |
2 |
1
|
eleq2d |
|- ( G e. ( RR ^pm RR ) -> ( F e. ( _O ` G ) <-> F e. { 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 |
|
dmeq |
|- ( f = F -> dom f = dom F ) |
4 |
3
|
ineq1d |
|- ( f = F -> ( dom f i^i ( x [,) +oo ) ) = ( dom F i^i ( x [,) +oo ) ) ) |
5 |
|
fveq1 |
|- ( f = F -> ( f ` y ) = ( F ` y ) ) |
6 |
5
|
breq1d |
|- ( f = F -> ( ( f ` y ) <_ ( m x. ( G ` y ) ) <-> ( F ` y ) <_ ( m x. ( G ` y ) ) ) ) |
7 |
4 6
|
raleqbidv |
|- ( f = F -> ( 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 ) ) ) ) |
8 |
7
|
2rexbidv |
|- ( f = F -> ( 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 ) ) ) ) |
9 |
8
|
elrab |
|- ( F e. { 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 ) ) ) ) |
10 |
2 9
|
syl6bb |
|- ( G e. ( RR ^pm RR ) -> ( F e. ( _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 ) ) ) ) ) |
11 |
10
|
pm5.32i |
|- ( ( G e. ( RR ^pm RR ) /\ F e. ( _O ` G ) ) <-> ( 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 ) ) ) ) ) |
12 |
|
elbigofrcl |
|- ( F e. ( _O ` G ) -> G e. ( RR ^pm RR ) ) |
13 |
12
|
pm4.71ri |
|- ( F e. ( _O ` G ) <-> ( G e. ( RR ^pm RR ) /\ F e. ( _O ` G ) ) ) |
14 |
|
3anan12 |
|- ( ( 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 ) ) ) <-> ( 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 ) ) ) ) ) |
15 |
11 13 14
|
3bitr4i |
|- ( 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 ) ) ) ) |