Step |
Hyp |
Ref |
Expression |
1 |
|
o1le.1 |
|- ( ph -> M e. RR ) |
2 |
|
o1le.2 |
|- ( ph -> ( x e. A |-> B ) e. O(1) ) |
3 |
|
o1le.3 |
|- ( ( ph /\ x e. A ) -> B e. V ) |
4 |
|
o1le.4 |
|- ( ( ph /\ x e. A ) -> C e. CC ) |
5 |
|
o1le.5 |
|- ( ( ph /\ ( x e. A /\ M <_ x ) ) -> ( abs ` C ) <_ ( abs ` B ) ) |
6 |
3 2
|
o1mptrcl |
|- ( ( ph /\ x e. A ) -> B e. CC ) |
7 |
6
|
lo1o12 |
|- ( ph -> ( ( x e. A |-> B ) e. O(1) <-> ( x e. A |-> ( abs ` B ) ) e. <_O(1) ) ) |
8 |
2 7
|
mpbid |
|- ( ph -> ( x e. A |-> ( abs ` B ) ) e. <_O(1) ) |
9 |
|
fvexd |
|- ( ( ph /\ x e. A ) -> ( abs ` B ) e. _V ) |
10 |
4
|
abscld |
|- ( ( ph /\ x e. A ) -> ( abs ` C ) e. RR ) |
11 |
1 8 9 10 5
|
lo1le |
|- ( ph -> ( x e. A |-> ( abs ` C ) ) e. <_O(1) ) |
12 |
4
|
lo1o12 |
|- ( ph -> ( ( x e. A |-> C ) e. O(1) <-> ( x e. A |-> ( abs ` C ) ) e. <_O(1) ) ) |
13 |
11 12
|
mpbird |
|- ( ph -> ( x e. A |-> C ) e. O(1) ) |