Metamath Proof Explorer


Theorem infxrss

Description: Larger sets of extended reals have smaller infima. (Contributed by Glauco Siliprandi, 11-Dec-2019) (Revised by AV, 13-Sep-2020)

Ref Expression
Assertion infxrss
|- ( ( A C_ B /\ B C_ RR* ) -> inf ( B , RR* , < ) <_ inf ( A , RR* , < ) )

Proof

Step Hyp Ref Expression
1 simplr
 |-  ( ( ( A C_ B /\ B C_ RR* ) /\ x e. A ) -> B C_ RR* )
2 simpl
 |-  ( ( A C_ B /\ B C_ RR* ) -> A C_ B )
3 2 sselda
 |-  ( ( ( A C_ B /\ B C_ RR* ) /\ x e. A ) -> x e. B )
4 infxrlb
 |-  ( ( B C_ RR* /\ x e. B ) -> inf ( B , RR* , < ) <_ x )
5 1 3 4 syl2anc
 |-  ( ( ( A C_ B /\ B C_ RR* ) /\ x e. A ) -> inf ( B , RR* , < ) <_ x )
6 5 ralrimiva
 |-  ( ( A C_ B /\ B C_ RR* ) -> A. x e. A inf ( B , RR* , < ) <_ x )
7 sstr
 |-  ( ( A C_ B /\ B C_ RR* ) -> A C_ RR* )
8 infxrcl
 |-  ( B C_ RR* -> inf ( B , RR* , < ) e. RR* )
9 8 adantl
 |-  ( ( A C_ B /\ B C_ RR* ) -> inf ( B , RR* , < ) e. RR* )
10 infxrgelb
 |-  ( ( A C_ RR* /\ inf ( B , RR* , < ) e. RR* ) -> ( inf ( B , RR* , < ) <_ inf ( A , RR* , < ) <-> A. x e. A inf ( B , RR* , < ) <_ x ) )
11 7 9 10 syl2anc
 |-  ( ( A C_ B /\ B C_ RR* ) -> ( inf ( B , RR* , < ) <_ inf ( A , RR* , < ) <-> A. x e. A inf ( B , RR* , < ) <_ x ) )
12 6 11 mpbird
 |-  ( ( A C_ B /\ B C_ RR* ) -> inf ( B , RR* , < ) <_ inf ( A , RR* , < ) )