Metamath Proof Explorer

Theorem limsupgord

Description: Ordering property of the superior limit function. (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by Mario Carneiro, 7-May-2016)

Ref Expression
Assertion limsupgord 
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> sup ( ( ( F " ( B [,) +oo ) ) i^i RR* ) , RR* , < ) <_ sup ( ( ( F " ( A [,) +oo ) ) i^i RR* ) , RR* , < ) )

Proof

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* , < ) )