Metamath Proof Explorer

Theorem infxrunb3

Description: The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Step	Hyp	Ref	Expression
1		unb2ltle	\|- ( A C_ RR* -> ( A. w e. RR E. y e. A y < w <-> A. x e. RR E. y e. A y <_ x ) )
2		infxrunb2	\|- ( A C_ RR* -> ( A. w e. RR E. y e. A y < w <-> inf ( A , RR* , < ) = -oo ) )
3	1 2	bitr3d	\|- ( A C_ RR* -> ( A. x e. RR E. y e. A y <_ x <-> inf ( A , RR* , < ) = -oo ) )

Step

Hyp

Ref

Expression

 |-  ( A C_ RR* -> ( A. w e. RR E. y e. A y < w <-> A. x e. RR E. y e. A y <_ x ) )

 |-  ( A C_ RR* -> ( A. w e. RR E. y e. A y < w <-> inf ( A , RR* , < ) = -oo ) )

1 2

 |-  ( A C_ RR* -> ( A. x e. RR E. y e. A y <_ x <-> inf ( A , RR* , < ) = -oo ) )