Metamath Proof Explorer

Theorem elbigo

Description: Properties of a function of order G(x). (Contributed by AV, 16-May-2020)

Ref Expression
Assertion 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 ) ) ) )

Proof

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 bitrdi 
 |-  ( 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 ) ) ) )