# Metamath Proof Explorer

## Theorem xrinf0

Description: The infimum of the empty set under the extended reals is positive infinity. (Contributed by Mario Carneiro, 21-Apr-2015) (Revised by AV, 5-Sep-2020)

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

### Proof

Step Hyp Ref Expression
1 xrltso ${⊢}<\mathrm{Or}{ℝ}^{*}$
2 1 a1i ${⊢}\top \to <\mathrm{Or}{ℝ}^{*}$
3 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
4 3 a1i ${⊢}\top \to \mathrm{+\infty }\in {ℝ}^{*}$
5 noel ${⊢}¬{y}\in \varnothing$
6 5 pm2.21i ${⊢}{y}\in \varnothing \to ¬{y}<\mathrm{+\infty }$
7 6 adantl ${⊢}\left(\top \wedge {y}\in \varnothing \right)\to ¬{y}<\mathrm{+\infty }$
8 pnfnlt ${⊢}{y}\in {ℝ}^{*}\to ¬\mathrm{+\infty }<{y}$
9 8 pm2.21d ${⊢}{y}\in {ℝ}^{*}\to \left(\mathrm{+\infty }<{y}\to \exists {z}\in \varnothing \phantom{\rule{.4em}{0ex}}{z}<{y}\right)$
10 9 imp ${⊢}\left({y}\in {ℝ}^{*}\wedge \mathrm{+\infty }<{y}\right)\to \exists {z}\in \varnothing \phantom{\rule{.4em}{0ex}}{z}<{y}$
11 10 adantl ${⊢}\left(\top \wedge \left({y}\in {ℝ}^{*}\wedge \mathrm{+\infty }<{y}\right)\right)\to \exists {z}\in \varnothing \phantom{\rule{.4em}{0ex}}{z}<{y}$
12 2 4 7 11 eqinfd ${⊢}\top \to sup\left(\varnothing ,{ℝ}^{*},<\right)=\mathrm{+\infty }$
13 12 mptru ${⊢}sup\left(\varnothing ,{ℝ}^{*},<\right)=\mathrm{+\infty }$