Step |
Hyp |
Ref |
Expression |
1 |
|
icco1.1 |
|- ( ph -> A C_ RR ) |
2 |
|
icco1.2 |
|- ( ( ph /\ x e. A ) -> B e. RR ) |
3 |
|
icco1.3 |
|- ( ph -> C e. RR ) |
4 |
|
icco1.4 |
|- ( ph -> M e. RR ) |
5 |
|
icco1.5 |
|- ( ph -> N e. RR ) |
6 |
|
icco1.6 |
|- ( ( ph /\ ( x e. A /\ C <_ x ) ) -> B e. ( M [,] N ) ) |
7 |
|
elicc2 |
|- ( ( M e. RR /\ N e. RR ) -> ( B e. ( M [,] N ) <-> ( B e. RR /\ M <_ B /\ B <_ N ) ) ) |
8 |
4 5 7
|
syl2anc |
|- ( ph -> ( B e. ( M [,] N ) <-> ( B e. RR /\ M <_ B /\ B <_ N ) ) ) |
9 |
8
|
adantr |
|- ( ( ph /\ ( x e. A /\ C <_ x ) ) -> ( B e. ( M [,] N ) <-> ( B e. RR /\ M <_ B /\ B <_ N ) ) ) |
10 |
6 9
|
mpbid |
|- ( ( ph /\ ( x e. A /\ C <_ x ) ) -> ( B e. RR /\ M <_ B /\ B <_ N ) ) |
11 |
10
|
simp3d |
|- ( ( ph /\ ( x e. A /\ C <_ x ) ) -> B <_ N ) |
12 |
1 2 3 5 11
|
ello1d |
|- ( ph -> ( x e. A |-> B ) e. <_O(1) ) |
13 |
2
|
renegcld |
|- ( ( ph /\ x e. A ) -> -u B e. RR ) |
14 |
4
|
renegcld |
|- ( ph -> -u M e. RR ) |
15 |
10
|
simp2d |
|- ( ( ph /\ ( x e. A /\ C <_ x ) ) -> M <_ B ) |
16 |
4
|
adantr |
|- ( ( ph /\ ( x e. A /\ C <_ x ) ) -> M e. RR ) |
17 |
2
|
adantrr |
|- ( ( ph /\ ( x e. A /\ C <_ x ) ) -> B e. RR ) |
18 |
16 17
|
lenegd |
|- ( ( ph /\ ( x e. A /\ C <_ x ) ) -> ( M <_ B <-> -u B <_ -u M ) ) |
19 |
15 18
|
mpbid |
|- ( ( ph /\ ( x e. A /\ C <_ x ) ) -> -u B <_ -u M ) |
20 |
1 13 3 14 19
|
ello1d |
|- ( ph -> ( x e. A |-> -u B ) e. <_O(1) ) |
21 |
2
|
o1lo1 |
|- ( ph -> ( ( x e. A |-> B ) e. O(1) <-> ( ( x e. A |-> B ) e. <_O(1) /\ ( x e. A |-> -u B ) e. <_O(1) ) ) ) |
22 |
12 20 21
|
mpbir2and |
|- ( ph -> ( x e. A |-> B ) e. O(1) ) |