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		0red	$$⊢x=\mathrm{+\infty }\to 0\in ℝ$$
6		breq1	$$⊢y=0\to \left(y<x\leftrightarrow 0<x\right)$$
7	6	adantl	$$⊢\left(x=\mathrm{+\infty }\wedge y=0\right)\to \left(y<x\leftrightarrow 0<x\right)$$
8		0ltpnf	$$⊢0<\mathrm{+\infty }$$
9		breq2	$$⊢x=\mathrm{+\infty }\to \left(0<x\leftrightarrow 0<\mathrm{+\infty }\right)$$
10	8 9	mpbiri	$$⊢x=\mathrm{+\infty }\to 0<x$$
11	5 7 10	rspcedvd	$$⊢x=\mathrm{+\infty }\to \exists y\in ℝy<x$$
12	11	a1d	$$⊢x=\mathrm{+\infty }\to \left(\mathrm{-\infty }<x\to \exists y\in ℝy<x\right)$$
13		breq2	$$⊢x=\mathrm{-\infty }\to \left(\mathrm{-\infty }<x\leftrightarrow \mathrm{-\infty }<\mathrm{-\infty }\right)$$
14		mnfxr	$$⊢\mathrm{-\infty }\in {ℝ}^{*}$$
15		nltmnf	$$⊢\mathrm{-\infty }\in {ℝ}^{*}\to \neg \mathrm{-\infty }<\mathrm{-\infty }$$
16	15	pm2.21d	$$⊢\mathrm{-\infty }\in {ℝ}^{*}\to \left(\mathrm{-\infty }<\mathrm{-\infty }\to \exists y\in ℝy<x\right)$$
17	14 16	ax-mp	$$⊢\mathrm{-\infty }<\mathrm{-\infty }\to \exists y\in ℝy<x$$
18	13 17	syl6bi	$$⊢x=\mathrm{-\infty }\to \left(\mathrm{-\infty }<x\to \exists y\in ℝy<x\right)$$
19	4 12 18	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)$$
20	1 19	sylbi	$$⊢x\in {ℝ}^{*}\to \left(\mathrm{-\infty }<x\to \exists y\in ℝy<x\right)$$
21	20	rgen	$$⊢\forall x\in {ℝ}^{*}\left(\mathrm{-\infty }<x\to \exists y\in ℝy<x\right)$$