Metamath Proof Explorer

Theorem infrefilb

Description: The infimum of a finite set of reals is less than or equal to any of its elements. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Assertion infrefilb 
|- ( ( B C_ RR /\ B e. Fin /\ A e. B ) -> inf ( B , RR , < ) <_ A )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( B C_ RR /\ B e. Fin /\ A e. B ) -> B C_ RR )
2 fiminre2 
 |-  ( ( B C_ RR /\ B e. Fin ) -> E. x e. RR A. y e. B x <_ y )
3 2 3adant3 
 |-  ( ( B C_ RR /\ B e. Fin /\ A e. B ) -> E. x e. RR A. y e. B x <_ y )
4 simp3 
 |-  ( ( B C_ RR /\ B e. Fin /\ A e. B ) -> A e. B )
5 infrelb 
 |-  ( ( B C_ RR /\ E. x e. RR A. y e. B x <_ y /\ A e. B ) -> inf ( B , RR , < ) <_ A )
6 1 3 4 5 syl3anc 
 |-  ( ( B C_ RR /\ B e. Fin /\ A e. B ) -> inf ( B , RR , < ) <_ A )