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