Step |
Hyp |
Ref |
Expression |
1 |
|
o1dm |
|- ( F e. O(1) -> dom F C_ RR ) |
2 |
|
fdm |
|- ( F : A --> CC -> dom F = A ) |
3 |
2
|
sseq1d |
|- ( F : A --> CC -> ( dom F C_ RR <-> A C_ RR ) ) |
4 |
1 3
|
syl5ib |
|- ( F : A --> CC -> ( F e. O(1) -> A C_ RR ) ) |
5 |
|
lo1dm |
|- ( ( abs o. F ) e. <_O(1) -> dom ( abs o. F ) C_ RR ) |
6 |
|
absf |
|- abs : CC --> RR |
7 |
|
fco |
|- ( ( abs : CC --> RR /\ F : A --> CC ) -> ( abs o. F ) : A --> RR ) |
8 |
6 7
|
mpan |
|- ( F : A --> CC -> ( abs o. F ) : A --> RR ) |
9 |
8
|
fdmd |
|- ( F : A --> CC -> dom ( abs o. F ) = A ) |
10 |
9
|
sseq1d |
|- ( F : A --> CC -> ( dom ( abs o. F ) C_ RR <-> A C_ RR ) ) |
11 |
5 10
|
syl5ib |
|- ( F : A --> CC -> ( ( abs o. F ) e. <_O(1) -> A C_ RR ) ) |
12 |
|
fvco3 |
|- ( ( F : A --> CC /\ y e. A ) -> ( ( abs o. F ) ` y ) = ( abs ` ( F ` y ) ) ) |
13 |
12
|
adantlr |
|- ( ( ( F : A --> CC /\ A C_ RR ) /\ y e. A ) -> ( ( abs o. F ) ` y ) = ( abs ` ( F ` y ) ) ) |
14 |
13
|
breq1d |
|- ( ( ( F : A --> CC /\ A C_ RR ) /\ y e. A ) -> ( ( ( abs o. F ) ` y ) <_ m <-> ( abs ` ( F ` y ) ) <_ m ) ) |
15 |
14
|
imbi2d |
|- ( ( ( F : A --> CC /\ A C_ RR ) /\ y e. A ) -> ( ( x <_ y -> ( ( abs o. F ) ` y ) <_ m ) <-> ( x <_ y -> ( abs ` ( F ` y ) ) <_ m ) ) ) |
16 |
15
|
ralbidva |
|- ( ( F : A --> CC /\ A C_ RR ) -> ( A. y e. A ( x <_ y -> ( ( abs o. F ) ` y ) <_ m ) <-> A. y e. A ( x <_ y -> ( abs ` ( F ` y ) ) <_ m ) ) ) |
17 |
16
|
2rexbidv |
|- ( ( F : A --> CC /\ A C_ RR ) -> ( E. x e. RR E. m e. RR A. y e. A ( x <_ y -> ( ( abs o. F ) ` y ) <_ m ) <-> E. x e. RR E. m e. RR A. y e. A ( x <_ y -> ( abs ` ( F ` y ) ) <_ m ) ) ) |
18 |
|
ello12 |
|- ( ( ( abs o. F ) : A --> RR /\ A C_ RR ) -> ( ( abs o. F ) e. <_O(1) <-> E. x e. RR E. m e. RR A. y e. A ( x <_ y -> ( ( abs o. F ) ` y ) <_ m ) ) ) |
19 |
8 18
|
sylan |
|- ( ( F : A --> CC /\ A C_ RR ) -> ( ( abs o. F ) e. <_O(1) <-> E. x e. RR E. m e. RR A. y e. A ( x <_ y -> ( ( abs o. F ) ` y ) <_ m ) ) ) |
20 |
|
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 ) ) ) |
21 |
17 19 20
|
3bitr4rd |
|- ( ( F : A --> CC /\ A C_ RR ) -> ( F e. O(1) <-> ( abs o. F ) e. <_O(1) ) ) |
22 |
21
|
ex |
|- ( F : A --> CC -> ( A C_ RR -> ( F e. O(1) <-> ( abs o. F ) e. <_O(1) ) ) ) |
23 |
4 11 22
|
pm5.21ndd |
|- ( F : A --> CC -> ( F e. O(1) <-> ( abs o. F ) e. <_O(1) ) ) |