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 ℝ^{*} (−∞ < x \to \exists y \in ℝ y < x)$

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

Metamath Proof Explorer