Step |
Hyp |
Ref |
Expression |
1 |
|
lo1o12.1 |
|- ( ( ph /\ x e. A ) -> B e. CC ) |
2 |
1
|
fmpttd |
|- ( ph -> ( x e. A |-> B ) : A --> CC ) |
3 |
|
lo1o1 |
|- ( ( x e. A |-> B ) : A --> CC -> ( ( x e. A |-> B ) e. O(1) <-> ( abs o. ( x e. A |-> B ) ) e. <_O(1) ) ) |
4 |
2 3
|
syl |
|- ( ph -> ( ( x e. A |-> B ) e. O(1) <-> ( abs o. ( x e. A |-> B ) ) e. <_O(1) ) ) |
5 |
|
absf |
|- abs : CC --> RR |
6 |
5
|
a1i |
|- ( ph -> abs : CC --> RR ) |
7 |
6 1
|
cofmpt |
|- ( ph -> ( abs o. ( x e. A |-> B ) ) = ( x e. A |-> ( abs ` B ) ) ) |
8 |
7
|
eleq1d |
|- ( ph -> ( ( abs o. ( x e. A |-> B ) ) e. <_O(1) <-> ( x e. A |-> ( abs ` B ) ) e. <_O(1) ) ) |
9 |
4 8
|
bitrd |
|- ( ph -> ( ( x e. A |-> B ) e. O(1) <-> ( x e. A |-> ( abs ` B ) ) e. <_O(1) ) ) |