Metamath Proof Explorer

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 0red ⊢ ( 𝑥 = +∞ → 0 ∈ ℝ )
6 breq1 ⊢ ( 𝑦 = 0 → ( 𝑦 < 𝑥 ↔ 0 < 𝑥 ) )
7 6 adantl ⊢ ( ( 𝑥 = +∞ ∧ 𝑦 = 0 ) → ( 𝑦 < 𝑥 ↔ 0 < 𝑥 ) )
8 0ltpnf ⊢ 0 < +∞
9 breq2 ⊢ ( 𝑥 = +∞ → ( 0 < 𝑥 ↔ 0 < +∞ ) )
10 8 9 mpbiri ⊢ ( 𝑥 = +∞ → 0 < 𝑥 )
11 5 7 10 rspcedvd ⊢ ( 𝑥 = +∞ → ∃ 𝑦 ∈ ℝ 𝑦 < 𝑥 )
12 11 a1d ⊢ ( 𝑥 = +∞ → ( -∞ < 𝑥 → ∃ 𝑦 ∈ ℝ 𝑦 < 𝑥 ) )
13 breq2 ⊢ ( 𝑥 = -∞ → ( -∞ < 𝑥 ↔ -∞ < -∞ ) )
14 mnfxr ⊢ -∞ ∈ ℝ*
15 nltmnf ⊢ ( -∞ ∈ ℝ* → ¬ -∞ < -∞ )
16 15 pm2.21d ⊢ ( -∞ ∈ ℝ* → ( -∞ < -∞ → ∃ 𝑦 ∈ ℝ 𝑦 < 𝑥 ) )
17 14 16 ax-mp ⊢ ( -∞ < -∞ → ∃ 𝑦 ∈ ℝ 𝑦 < 𝑥 )
18 13 17 syl6bi ⊢ ( 𝑥 = -∞ → ( -∞ < 𝑥 → ∃ 𝑦 ∈ ℝ 𝑦 < 𝑥 ) )
19 4 12 18 3jaoi ⊢ ( ( 𝑥 ∈ ℝ ∨ 𝑥 = +∞ ∨ 𝑥 = -∞ ) → ( -∞ < 𝑥 → ∃ 𝑦 ∈ ℝ 𝑦 < 𝑥 ) )
20 1 19 sylbi ⊢ ( 𝑥 ∈ ℝ* → ( -∞ < 𝑥 → ∃ 𝑦 ∈ ℝ 𝑦 < 𝑥 ) )
21 20 rgen ⊢ ∀ 𝑥 ∈ ℝ* ( -∞ < 𝑥 → ∃ 𝑦 ∈ ℝ 𝑦 < 𝑥 )