Theorem infxrbnd2

Description: The infimum of a bounded-below set of extended reals is greater than minus infinity. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Assertion	infxrbnd2	$$⊢A\subseteq {ℝ}^{*}\to \left(\exists x\in ℝ\forall y\in Ax\le y\leftrightarrow \mathrm{-\infty }<inf\left(A,{ℝ}^{*},<\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ralnex	$$⊢\forall x\in ℝ\neg \forall y\in Ax\le y\leftrightarrow \neg \exists x\in ℝ\forall y\in Ax\le y$$
2		ssel2	$$⊢\left(A\subseteq {ℝ}^{*}\wedge y\in A\right)\to y\in {ℝ}^{*}$$
3		rexr	$$⊢x\in ℝ\to x\in {ℝ}^{*}$$
4		simpl	$$⊢\left(y\in {ℝ}^{*}\wedge x\in {ℝ}^{*}\right)\to y\in {ℝ}^{*}$$
5		simpr	$$⊢\left(y\in {ℝ}^{*}\wedge x\in {ℝ}^{*}\right)\to x\in {ℝ}^{*}$$
6	4 5	xrltnled	$$⊢\left(y\in {ℝ}^{*}\wedge x\in {ℝ}^{*}\right)\to \left(y<x\leftrightarrow \neg x\le y\right)$$
7	2 3 6	syl2an	$$⊢\left(\left(A\subseteq {ℝ}^{*}\wedge y\in A\right)\wedge x\in ℝ\right)\to \left(y<x\leftrightarrow \neg x\le y\right)$$
8	7	an32s	$$⊢\left(\left(A\subseteq {ℝ}^{*}\wedge x\in ℝ\right)\wedge y\in A\right)\to \left(y<x\leftrightarrow \neg x\le y\right)$$
9	8	rexbidva	$$⊢\left(A\subseteq {ℝ}^{*}\wedge x\in ℝ\right)\to \left(\exists y\in Ay<x\leftrightarrow \exists y\in A\neg x\le y\right)$$
10		rexnal	$$⊢\exists y\in A\neg x\le y\leftrightarrow \neg \forall y\in Ax\le y$$
11	9 10	bitr2di	$$⊢\left(A\subseteq {ℝ}^{*}\wedge x\in ℝ\right)\to \left(\neg \forall y\in Ax\le y\leftrightarrow \exists y\in Ay<x\right)$$
12	11	ralbidva	$$⊢A\subseteq {ℝ}^{*}\to \left(\forall x\in ℝ\neg \forall y\in Ax\le y\leftrightarrow \forall x\in ℝ\exists y\in Ay<x\right)$$
13	1 12	bitr3id	$$⊢A\subseteq {ℝ}^{*}\to \left(\neg \exists x\in ℝ\forall y\in Ax\le y\leftrightarrow \forall x\in ℝ\exists y\in Ay<x\right)$$
14		infxrunb2	$$⊢A\subseteq {ℝ}^{*}\to \left(\forall x\in ℝ\exists y\in Ay<x\leftrightarrow inf\left(A,{ℝ}^{*},<\right)=\mathrm{-\infty }\right)$$
15		infxrcl	$$⊢A\subseteq {ℝ}^{*}\to inf\left(A,{ℝ}^{*},<\right)\in {ℝ}^{*}$$
16		ngtmnft	$$⊢inf\left(A,{ℝ}^{*},<\right)\in {ℝ}^{*}\to \left(inf\left(A,{ℝ}^{*},<\right)=\mathrm{-\infty }\leftrightarrow \neg \mathrm{-\infty }<inf\left(A,{ℝ}^{*},<\right)\right)$$
17	15 16	syl	$$⊢A\subseteq {ℝ}^{*}\to \left(inf\left(A,{ℝ}^{*},<\right)=\mathrm{-\infty }\leftrightarrow \neg \mathrm{-\infty }<inf\left(A,{ℝ}^{*},<\right)\right)$$
18	13 14 17	3bitrd	$$⊢A\subseteq {ℝ}^{*}\to \left(\neg \exists x\in ℝ\forall y\in Ax\le y\leftrightarrow \neg \mathrm{-\infty }<inf\left(A,{ℝ}^{*},<\right)\right)$$
19	18	con4bid	$$⊢A\subseteq {ℝ}^{*}\to \left(\exists x\in ℝ\forall y\in Ax\le y\leftrightarrow \mathrm{-\infty }<inf\left(A,{ℝ}^{*},<\right)\right)$$