Theorem infrecl

Description: Closure of infimum of a nonempty bounded set of reals. (Contributed by NM, 8-Oct-2005) (Revised by AV, 4-Sep-2020)

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

Proof

Step	Hyp	Ref	Expression
1		ltso	|- < Or RR
2	1	a1i	|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) -> < Or RR )
3		infm3	|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) -> E. x e. RR ( A. y e. A -. y < x /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) )
4	2 3	infcl	|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) -> inf ( A , RR , < ) e. RR )