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 ‘ ∅ ) = -∞

Metamath Proof Explorer

Theorem limsup0

Proof