Metamath Proof Explorer

Theorem elo1

Description: Elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 15-Sep-2014)

Ref Expression
Assertion elo1 
|- ( F e. O(1) <-> ( F e. ( CC ^pm RR ) /\ E. x e. RR E. m e. RR A. y e. ( dom F i^i ( x [,) +oo ) ) ( abs ` ( 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 fveq2d 
 |-  ( f = F -> ( abs ` ( f ` y ) ) = ( abs ` ( F ` y ) ) )
5 4 breq1d 
 |-  ( f = F -> ( ( abs ` ( f ` y ) ) <_ m <-> ( abs ` ( F ` y ) ) <_ m ) )
6 2 5 raleqbidv 
 |-  ( f = F -> ( A. y e. ( dom f i^i ( x [,) +oo ) ) ( abs ` ( f ` y ) ) <_ m <-> A. y e. ( dom F i^i ( x [,) +oo ) ) ( abs ` ( F ` y ) ) <_ m ) )
7 6 2rexbidv 
 |-  ( f = F -> ( E. x e. RR E. m e. RR A. y e. ( dom f i^i ( x [,) +oo ) ) ( abs ` ( f ` y ) ) <_ m <-> E. x e. RR E. m e. RR A. y e. ( dom F i^i ( x [,) +oo ) ) ( abs ` ( F ` y ) ) <_ m ) )
8 df-o1 
 |-  O(1) = { f e. ( CC ^pm RR ) | E. x e. RR E. m e. RR A. y e. ( dom f i^i ( x [,) +oo ) ) ( abs ` ( f ` y ) ) <_ m }
9 7 8 elrab2 
 |-  ( F e. O(1) <-> ( F e. ( CC ^pm RR ) /\ E. x e. RR E. m e. RR A. y e. ( dom F i^i ( x [,) +oo ) ) ( abs ` ( F ` y ) ) <_ m ) )