Metamath Proof Explorer

Theorem elo12

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

Ref Expression
Assertion elo12 
|- ( ( F : A --> CC /\ A C_ RR ) -> ( F e. O(1) <-> E. x e. RR E. m e. RR A. y e. A ( x <_ y -> ( abs ` ( F ` y ) ) <_ m ) ) )

Proof

Step Hyp Ref Expression
1 cnex 
 |-  CC e. _V
2 reex 
 |-  RR e. _V
3 elpm2r 
 |-  ( ( ( CC e. _V /\ RR e. _V ) /\ ( F : A --> CC /\ A C_ RR ) ) -> F e. ( CC ^pm RR ) )
4 1 2 3 mpanl12 
 |-  ( ( F : A --> CC /\ A C_ RR ) -> F e. ( CC ^pm RR ) )
5 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 ) )
6 5 baib 
 |-  ( F e. ( CC ^pm RR ) -> ( F e. O(1) <-> E. x e. RR E. m e. RR A. y e. ( dom F i^i ( x [,) +oo ) ) ( abs ` ( F ` y ) ) <_ m ) )
7 4 6 syl 
 |-  ( ( F : A --> CC /\ A C_ RR ) -> ( F e. O(1) <-> E. x e. RR E. m e. RR A. y e. ( dom F i^i ( x [,) +oo ) ) ( abs ` ( F ` y ) ) <_ m ) )
8 elin 
 |-  ( y e. ( dom F i^i ( x [,) +oo ) ) <-> ( y e. dom F /\ y e. ( x [,) +oo ) ) )
9 fdm 
 |-  ( F : A --> CC -> dom F = A )
10 9 ad3antrrr 
 |-  ( ( ( ( F : A --> CC /\ A C_ RR ) /\ x e. RR ) /\ m e. RR ) -> dom F = A )
11 10 eleq2d 
 |-  ( ( ( ( F : A --> CC /\ A C_ RR ) /\ x e. RR ) /\ m e. RR ) -> ( y e. dom F <-> y e. A ) )
12 11 anbi1d 
 |-  ( ( ( ( F : A --> CC /\ A C_ RR ) /\ x e. RR ) /\ m e. RR ) -> ( ( y e. dom F /\ y e. ( x [,) +oo ) ) <-> ( y e. A /\ y e. ( x [,) +oo ) ) ) )
13 simpllr 
 |-  ( ( ( ( F : A --> CC /\ A C_ RR ) /\ x e. RR ) /\ m e. RR ) -> A C_ RR )
14 13 sselda 
 |-  ( ( ( ( ( F : A --> CC /\ A C_ RR ) /\ x e. RR ) /\ m e. RR ) /\ y e. A ) -> y e. RR )
15 simpllr 
 |-  ( ( ( ( ( F : A --> CC /\ A C_ RR ) /\ x e. RR ) /\ m e. RR ) /\ y e. A ) -> x e. RR )
16 elicopnf 
 |-  ( x e. RR -> ( y e. ( x [,) +oo ) <-> ( y e. RR /\ x <_ y ) ) )
17 15 16 syl 
 |-  ( ( ( ( ( F : A --> CC /\ A C_ RR ) /\ x e. RR ) /\ m e. RR ) /\ y e. A ) -> ( y e. ( x [,) +oo ) <-> ( y e. RR /\ x <_ y ) ) )
18 14 17 mpbirand 
 |-  ( ( ( ( ( F : A --> CC /\ A C_ RR ) /\ x e. RR ) /\ m e. RR ) /\ y e. A ) -> ( y e. ( x [,) +oo ) <-> x <_ y ) )
19 18 pm5.32da 
 |-  ( ( ( ( F : A --> CC /\ A C_ RR ) /\ x e. RR ) /\ m e. RR ) -> ( ( y e. A /\ y e. ( x [,) +oo ) ) <-> ( y e. A /\ x <_ y ) ) )
20 12 19 bitrd 
 |-  ( ( ( ( F : A --> CC /\ A C_ RR ) /\ x e. RR ) /\ m e. RR ) -> ( ( y e. dom F /\ y e. ( x [,) +oo ) ) <-> ( y e. A /\ x <_ y ) ) )
21 8 20 syl5bb 
 |-  ( ( ( ( F : A --> CC /\ A C_ RR ) /\ x e. RR ) /\ m e. RR ) -> ( y e. ( dom F i^i ( x [,) +oo ) ) <-> ( y e. A /\ x <_ y ) ) )
22 21 imbi1d 
 |-  ( ( ( ( F : A --> CC /\ A C_ RR ) /\ x e. RR ) /\ m e. RR ) -> ( ( y e. ( dom F i^i ( x [,) +oo ) ) -> ( abs ` ( F ` y ) ) <_ m ) <-> ( ( y e. A /\ x <_ y ) -> ( abs ` ( F ` y ) ) <_ m ) ) )
23 impexp 
 |-  ( ( ( y e. A /\ x <_ y ) -> ( abs ` ( F ` y ) ) <_ m ) <-> ( y e. A -> ( x <_ y -> ( abs ` ( F ` y ) ) <_ m ) ) )
24 22 23 bitrdi 
 |-  ( ( ( ( F : A --> CC /\ A C_ RR ) /\ x e. RR ) /\ m e. RR ) -> ( ( y e. ( dom F i^i ( x [,) +oo ) ) -> ( abs ` ( F ` y ) ) <_ m ) <-> ( y e. A -> ( x <_ y -> ( abs ` ( F ` y ) ) <_ m ) ) ) )
25 24 ralbidv2 
 |-  ( ( ( ( F : A --> CC /\ A C_ RR ) /\ x e. RR ) /\ m e. RR ) -> ( A. y e. ( dom F i^i ( x [,) +oo ) ) ( abs ` ( F ` y ) ) <_ m <-> A. y e. A ( x <_ y -> ( abs ` ( F ` y ) ) <_ m ) ) )
26 25 rexbidva 
 |-  ( ( ( F : A --> CC /\ A C_ RR ) /\ x e. RR ) -> ( E. m e. RR A. y e. ( dom F i^i ( x [,) +oo ) ) ( abs ` ( F ` y ) ) <_ m <-> E. m e. RR A. y e. A ( x <_ y -> ( abs ` ( F ` y ) ) <_ m ) ) )
27 26 rexbidva 
 |-  ( ( F : A --> CC /\ A C_ RR ) -> ( 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. A ( x <_ y -> ( abs ` ( F ` y ) ) <_ m ) ) )
28 7 27 bitrd 
 |-  ( ( F : A --> CC /\ A C_ RR ) -> ( F e. O(1) <-> E. x e. RR E. m e. RR A. y e. A ( x <_ y -> ( abs ` ( F ` y ) ) <_ m ) ) )