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	⊢ ∀ 𝑥 ∈ ℝ* ( -∞ < 𝑥 → ∃ 𝑦 ∈ ℝ 𝑦 < 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		elxr	⊢ ( 𝑥 ∈ ℝ* ↔ ( 𝑥 ∈ ℝ ∨ 𝑥 = +∞ ∨ 𝑥 = -∞ ) )
2		reltre	⊢ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑦 < 𝑥
3	2	rspec	⊢ ( 𝑥 ∈ ℝ → ∃ 𝑦 ∈ ℝ 𝑦 < 𝑥 )
4	3	a1d	⊢ ( 𝑥 ∈ ℝ → ( -∞ < 𝑥 → ∃ 𝑦 ∈ ℝ 𝑦 < 𝑥 ) )
5		breq1	⊢ ( 𝑦 = 0 → ( 𝑦 < 𝑥 ↔ 0 < 𝑥 ) )
6		0red	⊢ ( 𝑥 = +∞ → 0 ∈ ℝ )
7		0ltpnf	⊢ 0 < +∞
8		breq2	⊢ ( 𝑥 = +∞ → ( 0 < 𝑥 ↔ 0 < +∞ ) )
9	7 8	mpbiri	⊢ ( 𝑥 = +∞ → 0 < 𝑥 )
10	5 6 9	rspcedvdw	⊢ ( 𝑥 = +∞ → ∃ 𝑦 ∈ ℝ 𝑦 < 𝑥 )
11	10	a1d	⊢ ( 𝑥 = +∞ → ( -∞ < 𝑥 → ∃ 𝑦 ∈ ℝ 𝑦 < 𝑥 ) )
12		breq2	⊢ ( 𝑥 = -∞ → ( -∞ < 𝑥 ↔ -∞ < -∞ ) )
13		mnfxr	⊢ -∞ ∈ ℝ*
14		nltmnf	⊢ ( -∞ ∈ ℝ* → ¬ -∞ < -∞ )
15	14	pm2.21d	⊢ ( -∞ ∈ ℝ* → ( -∞ < -∞ → ∃ 𝑦 ∈ ℝ 𝑦 < 𝑥 ) )
16	13 15	ax-mp	⊢ ( -∞ < -∞ → ∃ 𝑦 ∈ ℝ 𝑦 < 𝑥 )
17	12 16	biimtrdi	⊢ ( 𝑥 = -∞ → ( -∞ < 𝑥 → ∃ 𝑦 ∈ ℝ 𝑦 < 𝑥 ) )
18	4 11 17	3jaoi	⊢ ( ( 𝑥 ∈ ℝ ∨ 𝑥 = +∞ ∨ 𝑥 = -∞ ) → ( -∞ < 𝑥 → ∃ 𝑦 ∈ ℝ 𝑦 < 𝑥 ) )
19	1 18	sylbi	⊢ ( 𝑥 ∈ ℝ* → ( -∞ < 𝑥 → ∃ 𝑦 ∈ ℝ 𝑦 < 𝑥 ) )
20	19	rgen	⊢ ∀ 𝑥 ∈ ℝ* ( -∞ < 𝑥 → ∃ 𝑦 ∈ ℝ 𝑦 < 𝑥 )