Metamath Proof Explorer

Theorem liminfgord

Description: Ordering property of the inferior limit function. (Contributed by Glauco Siliprandi, 2-Jan-2022)

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

Proof

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