Metamath Proof Explorer

Theorem ello1

Description: Elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Assertion ello1 
|- ( F e. <_O(1) <-> ( 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 ) )

Proof

Step Hyp Ref Expression
1 dmeq 
 |-  ( f = F -> dom f = dom F )
2 1 ineq1d 
 |-  ( f = F -> ( dom f i^i ( x [,) +oo ) ) = ( dom F i^i ( x [,) +oo ) ) )
3 fveq1 
 |-  ( f = F -> ( f ` y ) = ( F ` y ) )
4 3 breq1d 
 |-  ( f = F -> ( ( f ` y ) <_ m <-> ( F ` y ) <_ m ) )
5 2 4 raleqbidv 
 |-  ( f = F -> ( A. y e. ( dom f i^i ( x [,) +oo ) ) ( f ` y ) <_ m <-> A. y e. ( dom F i^i ( x [,) +oo ) ) ( F ` y ) <_ m ) )
6 5 2rexbidv 
 |-  ( f = F -> ( E. x e. RR E. m e. RR A. y e. ( dom f i^i ( x [,) +oo ) ) ( f ` y ) <_ m <-> E. x e. RR E. m e. RR A. y e. ( dom F i^i ( x [,) +oo ) ) ( F ` y ) <_ m ) )
7 df-lo1 
 |-  <_O(1) = { 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 }
8 6 7 elrab2 
 |-  ( F e. <_O(1) <-> ( 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 ) )