Theorem limsup0

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

	Ref	Expression
Assertion	limsup0	⊢ ( lim sup ‘ ∅ ) = -∞

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2		eqid	⊢ ( 𝑥 ∈ ℝ ↦ sup ( ( ( ∅ “ ( 𝑥 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑥 ∈ ℝ ↦ sup ( ( ( ∅ “ ( 𝑥 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
3	2	limsupval	⊢ ( ∅ ∈ V → ( lim sup ‘ ∅ ) = inf ( ran ( 𝑥 ∈ ℝ ↦ sup ( ( ( ∅ “ ( 𝑥 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
4	1 3	ax-mp	⊢ ( lim sup ‘ ∅ ) = inf ( ran ( 𝑥 ∈ ℝ ↦ sup ( ( ( ∅ “ ( 𝑥 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < )
5		0ima	⊢ ( ∅ “ ( 𝑥 [,) +∞ ) ) = ∅
6	5	ineq1i	⊢ ( ( ∅ “ ( 𝑥 [,) +∞ ) ) ∩ ℝ* ) = ( ∅ ∩ ℝ* )
7		0in	⊢ ( ∅ ∩ ℝ* ) = ∅
8	6 7	eqtri	⊢ ( ( ∅ “ ( 𝑥 [,) +∞ ) ) ∩ ℝ* ) = ∅
9	8	supeq1i	⊢ sup ( ( ( ∅ “ ( 𝑥 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) = sup ( ∅ , ℝ* , < )
10		xrsup0	⊢ sup ( ∅ , ℝ* , < ) = -∞
11	9 10	eqtri	⊢ sup ( ( ( ∅ “ ( 𝑥 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) = -∞
12	11	mpteq2i	⊢ ( 𝑥 ∈ ℝ ↦ sup ( ( ( ∅ “ ( 𝑥 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑥 ∈ ℝ ↦ -∞ )
13		ren0	⊢ ℝ ≠ ∅
14	13	a1i	⊢ ( ⊤ → ℝ ≠ ∅ )
15	12 14	rnmptc	⊢ ( ⊤ → ran ( 𝑥 ∈ ℝ ↦ sup ( ( ( ∅ “ ( 𝑥 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = { -∞ } )
16	15	mptru	⊢ ran ( 𝑥 ∈ ℝ ↦ sup ( ( ( ∅ “ ( 𝑥 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = { -∞ }
17	16	infeq1i	⊢ inf ( ran ( 𝑥 ∈ ℝ ↦ sup ( ( ( ∅ “ ( 𝑥 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) = inf ( { -∞ } , ℝ* , < )
18		xrltso	⊢ < Or ℝ*
19		mnfxr	⊢ -∞ ∈ ℝ*
20		infsn	⊢ ( ( < Or ℝ* ∧ -∞ ∈ ℝ* ) → inf ( { -∞ } , ℝ* , < ) = -∞ )
21	18 19 20	mp2an	⊢ inf ( { -∞ } , ℝ* , < ) = -∞
22	4 17 21	3eqtri	⊢ ( lim sup ‘ ∅ ) = -∞