# Metamath Proof Explorer

## Theorem infmremnf

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

Ref Expression
Assertion infmremnf ${⊢}sup\left(ℝ,{ℝ}^{*},<\right)=\mathrm{-\infty }$

### Proof

Step Hyp Ref Expression
1 reltxrnmnf ${⊢}\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\mathrm{-\infty }<{x}\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}{z}<{x}\right)$
2 xrltso ${⊢}<\mathrm{Or}{ℝ}^{*}$
3 2 a1i ${⊢}\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\mathrm{-\infty }<{x}\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}{z}<{x}\right)\to <\mathrm{Or}{ℝ}^{*}$
4 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
5 4 a1i ${⊢}\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\mathrm{-\infty }<{x}\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}{z}<{x}\right)\to \mathrm{-\infty }\in {ℝ}^{*}$
6 rexr ${⊢}{y}\in ℝ\to {y}\in {ℝ}^{*}$
7 nltmnf ${⊢}{y}\in {ℝ}^{*}\to ¬{y}<\mathrm{-\infty }$
8 6 7 syl ${⊢}{y}\in ℝ\to ¬{y}<\mathrm{-\infty }$
9 8 adantl ${⊢}\left(\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\mathrm{-\infty }<{x}\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}{z}<{x}\right)\wedge {y}\in ℝ\right)\to ¬{y}<\mathrm{-\infty }$
10 breq2 ${⊢}{x}={y}\to \left(\mathrm{-\infty }<{x}↔\mathrm{-\infty }<{y}\right)$
11 breq2 ${⊢}{x}={y}\to \left({z}<{x}↔{z}<{y}\right)$
12 11 rexbidv ${⊢}{x}={y}\to \left(\exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}{z}<{x}↔\exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}{z}<{y}\right)$
13 10 12 imbi12d ${⊢}{x}={y}\to \left(\left(\mathrm{-\infty }<{x}\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}{z}<{x}\right)↔\left(\mathrm{-\infty }<{y}\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
14 13 rspcv ${⊢}{y}\in {ℝ}^{*}\to \left(\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\mathrm{-\infty }<{x}\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}{z}<{x}\right)\to \left(\mathrm{-\infty }<{y}\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
15 14 com23 ${⊢}{y}\in {ℝ}^{*}\to \left(\mathrm{-\infty }<{y}\to \left(\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\mathrm{-\infty }<{x}\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}{z}<{x}\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
16 15 imp ${⊢}\left({y}\in {ℝ}^{*}\wedge \mathrm{-\infty }<{y}\right)\to \left(\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\mathrm{-\infty }<{x}\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}{z}<{x}\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}{z}<{y}\right)$
17 16 impcom ${⊢}\left(\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\mathrm{-\infty }<{x}\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}{z}<{x}\right)\wedge \left({y}\in {ℝ}^{*}\wedge \mathrm{-\infty }<{y}\right)\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}{z}<{y}$
18 3 5 9 17 eqinfd ${⊢}\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\mathrm{-\infty }<{x}\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}{z}<{x}\right)\to sup\left(ℝ,{ℝ}^{*},<\right)=\mathrm{-\infty }$
19 1 18 ax-mp ${⊢}sup\left(ℝ,{ℝ}^{*},<\right)=\mathrm{-\infty }$