This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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