Metamath Proof Explorer

Theorem lbinf

Description: If a set of reals contains a lower bound, the lower bound is its infimum. (Contributed by NM, 9-Oct-2005) (Revised by AV, 4-Sep-2020)

Ref Expression
Assertion lbinf 
|- ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> inf ( S , RR , < ) = ( iota_ x e. S A. y e. S x <_ y ) )

Proof

Step Hyp Ref Expression
1 ltso 
 |-  < Or RR
2 1 a1i 
 |-  ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> < Or RR )
3 lbcl 
 |-  ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> ( iota_ x e. S A. y e. S x <_ y ) e. S )
4 ssel 
 |-  ( S C_ RR -> ( ( iota_ x e. S A. y e. S x <_ y ) e. S -> ( iota_ x e. S A. y e. S x <_ y ) e. RR ) )
5 4 adantr 
 |-  ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> ( ( iota_ x e. S A. y e. S x <_ y ) e. S -> ( iota_ x e. S A. y e. S x <_ y ) e. RR ) )
6 3 5 mpd 
 |-  ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> ( iota_ x e. S A. y e. S x <_ y ) e. RR )
7 6 adantr 
 |-  ( ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) /\ z e. S ) -> ( iota_ x e. S A. y e. S x <_ y ) e. RR )
8 ssel2 
 |-  ( ( S C_ RR /\ z e. S ) -> z e. RR )
9 8 adantlr 
 |-  ( ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) /\ z e. S ) -> z e. RR )
10 lble 
 |-  ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y /\ z e. S ) -> ( iota_ x e. S A. y e. S x <_ y ) <_ z )
11 10 3expa 
 |-  ( ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) /\ z e. S ) -> ( iota_ x e. S A. y e. S x <_ y ) <_ z )
12 7 9 11 lensymd 
 |-  ( ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) /\ z e. S ) -> -. z < ( iota_ x e. S A. y e. S x <_ y ) )
13 2 6 3 12 infmin 
 |-  ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> inf ( S , RR , < ) = ( iota_ x e. S A. y e. S x <_ y ) )