This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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