Step |
Hyp |
Ref |
Expression |
1 |
|
rexr |
|- ( A e. RR -> A e. RR* ) |
2 |
1
|
3ad2ant1 |
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> A e. RR* ) |
3 |
|
simp3 |
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> A <_ B ) |
4 |
|
df-ico |
|- [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } ) |
5 |
|
xrletr |
|- ( ( A e. RR* /\ B e. RR* /\ w e. RR* ) -> ( ( A <_ B /\ B <_ w ) -> A <_ w ) ) |
6 |
4 4 5
|
ixxss1 |
|- ( ( A e. RR* /\ A <_ B ) -> ( B [,) +oo ) C_ ( A [,) +oo ) ) |
7 |
2 3 6
|
syl2anc |
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( B [,) +oo ) C_ ( A [,) +oo ) ) |
8 |
|
imass2 |
|- ( ( B [,) +oo ) C_ ( A [,) +oo ) -> ( F " ( B [,) +oo ) ) C_ ( F " ( A [,) +oo ) ) ) |
9 |
|
ssrin |
|- ( ( F " ( B [,) +oo ) ) C_ ( F " ( A [,) +oo ) ) -> ( ( F " ( B [,) +oo ) ) i^i RR* ) C_ ( ( F " ( A [,) +oo ) ) i^i RR* ) ) |
10 |
7 8 9
|
3syl |
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( ( F " ( B [,) +oo ) ) i^i RR* ) C_ ( ( F " ( A [,) +oo ) ) i^i RR* ) ) |
11 |
|
inss2 |
|- ( ( F " ( A [,) +oo ) ) i^i RR* ) C_ RR* |
12 |
|
supxrcl |
|- ( ( ( F " ( A [,) +oo ) ) i^i RR* ) C_ RR* -> sup ( ( ( F " ( A [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR* ) |
13 |
11 12
|
ax-mp |
|- sup ( ( ( F " ( A [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR* |
14 |
|
xrleid |
|- ( sup ( ( ( F " ( A [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR* -> sup ( ( ( F " ( A [,) +oo ) ) i^i RR* ) , RR* , < ) <_ sup ( ( ( F " ( A [,) +oo ) ) i^i RR* ) , RR* , < ) ) |
15 |
13 14
|
ax-mp |
|- sup ( ( ( F " ( A [,) +oo ) ) i^i RR* ) , RR* , < ) <_ sup ( ( ( F " ( A [,) +oo ) ) i^i RR* ) , RR* , < ) |
16 |
|
supxrleub |
|- ( ( ( ( F " ( A [,) +oo ) ) i^i RR* ) C_ RR* /\ sup ( ( ( F " ( A [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR* ) -> ( sup ( ( ( F " ( A [,) +oo ) ) i^i RR* ) , RR* , < ) <_ sup ( ( ( F " ( A [,) +oo ) ) i^i RR* ) , RR* , < ) <-> A. x e. ( ( F " ( A [,) +oo ) ) i^i RR* ) x <_ sup ( ( ( F " ( A [,) +oo ) ) i^i RR* ) , RR* , < ) ) ) |
17 |
11 13 16
|
mp2an |
|- ( sup ( ( ( F " ( A [,) +oo ) ) i^i RR* ) , RR* , < ) <_ sup ( ( ( F " ( A [,) +oo ) ) i^i RR* ) , RR* , < ) <-> A. x e. ( ( F " ( A [,) +oo ) ) i^i RR* ) x <_ sup ( ( ( F " ( A [,) +oo ) ) i^i RR* ) , RR* , < ) ) |
18 |
15 17
|
mpbi |
|- A. x e. ( ( F " ( A [,) +oo ) ) i^i RR* ) x <_ sup ( ( ( F " ( A [,) +oo ) ) i^i RR* ) , RR* , < ) |
19 |
|
ssralv |
|- ( ( ( F " ( B [,) +oo ) ) i^i RR* ) C_ ( ( F " ( A [,) +oo ) ) i^i RR* ) -> ( A. x e. ( ( F " ( A [,) +oo ) ) i^i RR* ) x <_ sup ( ( ( F " ( A [,) +oo ) ) i^i RR* ) , RR* , < ) -> A. x e. ( ( F " ( B [,) +oo ) ) i^i RR* ) x <_ sup ( ( ( F " ( A [,) +oo ) ) i^i RR* ) , RR* , < ) ) ) |
20 |
10 18 19
|
mpisyl |
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> A. x e. ( ( F " ( B [,) +oo ) ) i^i RR* ) x <_ sup ( ( ( F " ( A [,) +oo ) ) i^i RR* ) , RR* , < ) ) |
21 |
|
inss2 |
|- ( ( F " ( B [,) +oo ) ) i^i RR* ) C_ RR* |
22 |
|
supxrleub |
|- ( ( ( ( F " ( B [,) +oo ) ) i^i RR* ) C_ RR* /\ sup ( ( ( F " ( A [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR* ) -> ( sup ( ( ( F " ( B [,) +oo ) ) i^i RR* ) , RR* , < ) <_ sup ( ( ( F " ( A [,) +oo ) ) i^i RR* ) , RR* , < ) <-> A. x e. ( ( F " ( B [,) +oo ) ) i^i RR* ) x <_ sup ( ( ( F " ( A [,) +oo ) ) i^i RR* ) , RR* , < ) ) ) |
23 |
21 13 22
|
mp2an |
|- ( sup ( ( ( F " ( B [,) +oo ) ) i^i RR* ) , RR* , < ) <_ sup ( ( ( F " ( A [,) +oo ) ) i^i RR* ) , RR* , < ) <-> A. x e. ( ( F " ( B [,) +oo ) ) i^i RR* ) x <_ sup ( ( ( F " ( A [,) +oo ) ) i^i RR* ) , RR* , < ) ) |
24 |
20 23
|
sylibr |
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> sup ( ( ( F " ( B [,) +oo ) ) i^i RR* ) , RR* , < ) <_ sup ( ( ( F " ( A [,) +oo ) ) i^i RR* ) , RR* , < ) ) |