Metamath Proof Explorer

Theorem ello12

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

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

Proof

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