# Metamath Proof Explorer

## Theorem limsup0

Description: The superior limit of the empty set (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Assertion limsup0 ${⊢}\mathrm{lim sup}\left(\varnothing \right)=\mathrm{-\infty }$

### Proof

Step Hyp Ref Expression
1 0ex ${⊢}\varnothing \in \mathrm{V}$
2 eqid ${⊢}\left({x}\in ℝ⟼sup\left(\varnothing \left[\left[{x},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)=\left({x}\in ℝ⟼sup\left(\varnothing \left[\left[{x},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)$
3 2 limsupval ${⊢}\varnothing \in \mathrm{V}\to \mathrm{lim sup}\left(\varnothing \right)=sup\left(\mathrm{ran}\left({x}\in ℝ⟼sup\left(\varnothing \left[\left[{x},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right),{ℝ}^{*},<\right)$
4 1 3 ax-mp ${⊢}\mathrm{lim sup}\left(\varnothing \right)=sup\left(\mathrm{ran}\left({x}\in ℝ⟼sup\left(\varnothing \left[\left[{x},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right),{ℝ}^{*},<\right)$
5 0ima ${⊢}\varnothing \left[\left[{x},\mathrm{+\infty }\right)\right]=\varnothing$
6 5 ineq1i ${⊢}\varnothing \left[\left[{x},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}=\varnothing \cap {ℝ}^{*}$
7 0in ${⊢}\varnothing \cap {ℝ}^{*}=\varnothing$
8 6 7 eqtri ${⊢}\varnothing \left[\left[{x},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*}=\varnothing$
9 8 supeq1i ${⊢}sup\left(\varnothing \left[\left[{x},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)=sup\left(\varnothing ,{ℝ}^{*},<\right)$
10 xrsup0 ${⊢}sup\left(\varnothing ,{ℝ}^{*},<\right)=\mathrm{-\infty }$
11 9 10 eqtri ${⊢}sup\left(\varnothing \left[\left[{x},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)=\mathrm{-\infty }$
12 11 mpteq2i ${⊢}\left({x}\in ℝ⟼sup\left(\varnothing \left[\left[{x},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)=\left({x}\in ℝ⟼\mathrm{-\infty }\right)$
13 ren0 ${⊢}ℝ\ne \varnothing$
14 13 a1i ${⊢}\top \to ℝ\ne \varnothing$
15 12 14 rnmptc ${⊢}\top \to \mathrm{ran}\left({x}\in ℝ⟼sup\left(\varnothing \left[\left[{x},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)=\left\{\mathrm{-\infty }\right\}$
16 15 mptru ${⊢}\mathrm{ran}\left({x}\in ℝ⟼sup\left(\varnothing \left[\left[{x},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)=\left\{\mathrm{-\infty }\right\}$
17 16 infeq1i ${⊢}sup\left(\mathrm{ran}\left({x}\in ℝ⟼sup\left(\varnothing \left[\left[{x},\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right),{ℝ}^{*},<\right)=sup\left(\left\{\mathrm{-\infty }\right\},{ℝ}^{*},<\right)$
18 xrltso ${⊢}<\mathrm{Or}{ℝ}^{*}$
19 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
20 infsn ${⊢}\left(<\mathrm{Or}{ℝ}^{*}\wedge \mathrm{-\infty }\in {ℝ}^{*}\right)\to sup\left(\left\{\mathrm{-\infty }\right\},{ℝ}^{*},<\right)=\mathrm{-\infty }$
21 18 19 20 mp2an ${⊢}sup\left(\left\{\mathrm{-\infty }\right\},{ℝ}^{*},<\right)=\mathrm{-\infty }$
22 4 17 21 3eqtri ${⊢}\mathrm{lim sup}\left(\varnothing \right)=\mathrm{-\infty }$