Theorem reltxrnmnf

Description: For all extended real numbers not being minus infinity there is a smaller real number. (Contributed by AV, 5-Sep-2020)

	Ref	Expression
Assertion	reltxrnmnf	$$⊢\forall x\in {ℝ}^{*}\left(\mathrm{-\infty }<x\to \exists y\in ℝy<x\right)$$

Proof

Step	Hyp	Ref	Expression
1		elxr	$$⊢x\in {ℝ}^{*}\leftrightarrow \left(x\in ℝ\vee x=\mathrm{+\infty }\vee x=\mathrm{-\infty }\right)$$
2		reltre	$$⊢\forall x\in ℝ\exists y\in ℝy<x$$
3	2	rspec	$$⊢x\in ℝ\to \exists y\in ℝy<x$$
4	3	a1d	$$⊢x\in ℝ\to \left(\mathrm{-\infty }<x\to \exists y\in ℝy<x\right)$$
5		breq1	$$⊢y=0\to \left(y<x\leftrightarrow 0<x\right)$$
6		0red	$$⊢x=\mathrm{+\infty }\to 0\in ℝ$$
7		0ltpnf	$$⊢0<\mathrm{+\infty }$$
8		breq2	$$⊢x=\mathrm{+\infty }\to \left(0<x\leftrightarrow 0<\mathrm{+\infty }\right)$$
9	7 8	mpbiri	$$⊢x=\mathrm{+\infty }\to 0<x$$
10	5 6 9	rspcedvdw	$$⊢x=\mathrm{+\infty }\to \exists y\in ℝy<x$$
11	10	a1d	$$⊢x=\mathrm{+\infty }\to \left(\mathrm{-\infty }<x\to \exists y\in ℝy<x\right)$$
12		breq2	$$⊢x=\mathrm{-\infty }\to \left(\mathrm{-\infty }<x\leftrightarrow \mathrm{-\infty }<\mathrm{-\infty }\right)$$
13		mnfxr	$$⊢\mathrm{-\infty }\in {ℝ}^{*}$$
14		nltmnf	$$⊢\mathrm{-\infty }\in {ℝ}^{*}\to \neg \mathrm{-\infty }<\mathrm{-\infty }$$
15	14	pm2.21d	$$⊢\mathrm{-\infty }\in {ℝ}^{*}\to \left(\mathrm{-\infty }<\mathrm{-\infty }\to \exists y\in ℝy<x\right)$$
16	13 15	ax-mp	$$⊢\mathrm{-\infty }<\mathrm{-\infty }\to \exists y\in ℝy<x$$
17	12 16	biimtrdi	$$⊢x=\mathrm{-\infty }\to \left(\mathrm{-\infty }<x\to \exists y\in ℝy<x\right)$$
18	4 11 17	3jaoi	$$⊢\left(x\in ℝ\vee x=\mathrm{+\infty }\vee x=\mathrm{-\infty }\right)\to \left(\mathrm{-\infty }<x\to \exists y\in ℝy<x\right)$$
19	1 18	sylbi	$$⊢x\in {ℝ}^{*}\to \left(\mathrm{-\infty }<x\to \exists y\in ℝy<x\right)$$
20	19	rgen	$$⊢\forall x\in {ℝ}^{*}\left(\mathrm{-\infty }<x\to \exists y\in ℝy<x\right)$$