Metamath Proof Explorer

Theorem lo1res

Description: The restriction of an eventually upper bounded function is eventually upper bounded. (Contributed by Mario Carneiro, 15-Sep-2014)

Ref Expression
Assertion lo1res 
|- ( F e. <_O(1) -> ( F |` A ) e. <_O(1) )

Proof

Step Hyp Ref Expression
1 lo1f 
 |-  ( F e. <_O(1) -> F : dom F --> RR )
2 lo1bdd 
 |-  ( ( F e. <_O(1) /\ F : dom F --> RR ) -> E. x e. RR E. m e. RR A. y e. dom F ( x <_ y -> ( F ` y ) <_ m ) )
3 1 2 mpdan 
 |-  ( F e. <_O(1) -> E. x e. RR E. m e. RR A. y e. dom F ( x <_ y -> ( F ` y ) <_ m ) )
4 inss1 
 |-  ( dom F i^i A ) C_ dom F
5 ssralv 
 |-  ( ( dom F i^i A ) C_ dom F -> ( A. y e. dom F ( x <_ y -> ( F ` y ) <_ m ) -> A. y e. ( dom F i^i A ) ( x <_ y -> ( F ` y ) <_ m ) ) )
6 4 5 ax-mp 
 |-  ( A. y e. dom F ( x <_ y -> ( F ` y ) <_ m ) -> A. y e. ( dom F i^i A ) ( x <_ y -> ( F ` y ) <_ m ) )
7 elinel2 
 |-  ( y e. ( dom F i^i A ) -> y e. A )
8 7 fvresd 
 |-  ( y e. ( dom F i^i A ) -> ( ( F |` A ) ` y ) = ( F ` y ) )
9 8 breq1d 
 |-  ( y e. ( dom F i^i A ) -> ( ( ( F |` A ) ` y ) <_ m <-> ( F ` y ) <_ m ) )
10 9 imbi2d 
 |-  ( y e. ( dom F i^i A ) -> ( ( x <_ y -> ( ( F |` A ) ` y ) <_ m ) <-> ( x <_ y -> ( F ` y ) <_ m ) ) )
11 10 ralbiia 
 |-  ( A. y e. ( dom F i^i A ) ( x <_ y -> ( ( F |` A ) ` y ) <_ m ) <-> A. y e. ( dom F i^i A ) ( x <_ y -> ( F ` y ) <_ m ) )
12 6 11 sylibr 
 |-  ( A. y e. dom F ( x <_ y -> ( F ` y ) <_ m ) -> A. y e. ( dom F i^i A ) ( x <_ y -> ( ( F |` A ) ` y ) <_ m ) )
13 12 reximi 
 |-  ( E. m e. RR A. y e. dom F ( x <_ y -> ( F ` y ) <_ m ) -> E. m e. RR A. y e. ( dom F i^i A ) ( x <_ y -> ( ( F |` A ) ` y ) <_ m ) )
14 13 reximi 
 |-  ( E. x e. RR E. m e. RR A. y e. dom F ( x <_ y -> ( F ` y ) <_ m ) -> E. x e. RR E. m e. RR A. y e. ( dom F i^i A ) ( x <_ y -> ( ( F |` A ) ` y ) <_ m ) )
15 3 14 syl 
 |-  ( F e. <_O(1) -> E. x e. RR E. m e. RR A. y e. ( dom F i^i A ) ( x <_ y -> ( ( F |` A ) ` y ) <_ m ) )
16 fssres 
 |-  ( ( F : dom F --> RR /\ ( dom F i^i A ) C_ dom F ) -> ( F |` ( dom F i^i A ) ) : ( dom F i^i A ) --> RR )
17 1 4 16 sylancl 
 |-  ( F e. <_O(1) -> ( F |` ( dom F i^i A ) ) : ( dom F i^i A ) --> RR )
18 resres 
 |-  ( ( F |` dom F ) |` A ) = ( F |` ( dom F i^i A ) )
19 ffn 
 |-  ( F : dom F --> RR -> F Fn dom F )
20 fnresdm 
 |-  ( F Fn dom F -> ( F |` dom F ) = F )
21 1 19 20 3syl 
 |-  ( F e. <_O(1) -> ( F |` dom F ) = F )
22 21 reseq1d 
 |-  ( F e. <_O(1) -> ( ( F |` dom F ) |` A ) = ( F |` A ) )
23 18 22 eqtr3id 
 |-  ( F e. <_O(1) -> ( F |` ( dom F i^i A ) ) = ( F |` A ) )
24 23 feq1d 
 |-  ( F e. <_O(1) -> ( ( F |` ( dom F i^i A ) ) : ( dom F i^i A ) --> RR <-> ( F |` A ) : ( dom F i^i A ) --> RR ) )
25 17 24 mpbid 
 |-  ( F e. <_O(1) -> ( F |` A ) : ( dom F i^i A ) --> RR )
26 lo1dm 
 |-  ( F e. <_O(1) -> dom F C_ RR )
27 4 26 sstrid 
 |-  ( F e. <_O(1) -> ( dom F i^i A ) C_ RR )
28 ello12 
 |-  ( ( ( F |` A ) : ( dom F i^i A ) --> RR /\ ( dom F i^i A ) C_ RR ) -> ( ( F |` A ) e. <_O(1) <-> E. x e. RR E. m e. RR A. y e. ( dom F i^i A ) ( x <_ y -> ( ( F |` A ) ` y ) <_ m ) ) )
29 25 27 28 syl2anc 
 |-  ( F e. <_O(1) -> ( ( F |` A ) e. <_O(1) <-> E. x e. RR E. m e. RR A. y e. ( dom F i^i A ) ( x <_ y -> ( ( F |` A ) ` y ) <_ m ) ) )
30 15 29 mpbird 
 |-  ( F e. <_O(1) -> ( F |` A ) e. <_O(1) )