Metamath Proof Explorer

Theorem infmremnf

Description: The infimum of the reals is minus infinity. (Contributed by AV, 5-Sep-2020)

Ref Expression
Assertion infmremnf ⊢ inf ℝ ℝ * < = −∞

Proof

Step Hyp Ref Expression
1 reltxrnmnf ⊢ ∀ x ∈ ℝ * −∞ < x → ∃ z ∈ ℝ z < x
2 xrltso ⊢ < Or ℝ *
3 2 a1i ⊢ ∀ x ∈ ℝ * −∞ < x → ∃ z ∈ ℝ z < x → < Or ℝ *
4 mnfxr ⊢ −∞ ∈ ℝ *
5 4 a1i ⊢ ∀ x ∈ ℝ * −∞ < x → ∃ z ∈ ℝ z < x → −∞ ∈ ℝ *
6 rexr ⊢ y ∈ ℝ → y ∈ ℝ *
7 nltmnf ⊢ y ∈ ℝ * → ¬ y < −∞
8 6 7 syl ⊢ y ∈ ℝ → ¬ y < −∞
9 8 adantl ⊢ ∀ x ∈ ℝ * −∞ < x → ∃ z ∈ ℝ z < x ∧ y ∈ ℝ → ¬ y < −∞
10 breq2 ⊢ x = y → −∞ < x ↔ −∞ < y
11 breq2 ⊢ x = y → z < x ↔ z < y
12 11 rexbidv ⊢ x = y → ∃ z ∈ ℝ z < x ↔ ∃ z ∈ ℝ z < y
13 10 12 imbi12d ⊢ x = y → −∞ < x → ∃ z ∈ ℝ z < x ↔ −∞ < y → ∃ z ∈ ℝ z < y
14 13 rspcv ⊢ y ∈ ℝ * → ∀ x ∈ ℝ * −∞ < x → ∃ z ∈ ℝ z < x → −∞ < y → ∃ z ∈ ℝ z < y
15 14 com23 ⊢ y ∈ ℝ * → −∞ < y → ∀ x ∈ ℝ * −∞ < x → ∃ z ∈ ℝ z < x → ∃ z ∈ ℝ z < y
16 15 imp ⊢ y ∈ ℝ * ∧ −∞ < y → ∀ x ∈ ℝ * −∞ < x → ∃ z ∈ ℝ z < x → ∃ z ∈ ℝ z < y
17 16 impcom ⊢ ∀ x ∈ ℝ * −∞ < x → ∃ z ∈ ℝ z < x ∧ y ∈ ℝ * ∧ −∞ < y → ∃ z ∈ ℝ z < y
18 3 5 9 17 eqinfd ⊢ ∀ x ∈ ℝ * −∞ < x → ∃ z ∈ ℝ z < x → inf ℝ ℝ * < = −∞
19 1 18 ax-mp ⊢ inf ℝ ℝ * < = −∞