Theorem liminf0

Description: The inferior limit of the empty set. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Assertion	liminf0	⊢ ( lim inf ‘ ∅ ) = +∞

Proof

Step	Hyp	Ref	Expression
1		nftru	⊢ Ⅎ 𝑥 ⊤
2		0ex	⊢ ∅ ∈ V
3	2	a1i	⊢ ( ⊤ → ∅ ∈ V )
4		0red	⊢ ( ⊤ → 0 ∈ ℝ )
5		noel	⊢ ¬ 𝑥 ∈ ∅
6		elinel1	⊢ ( 𝑥 ∈ ( ∅ ∩ ( 0 [,) +∞ ) ) → 𝑥 ∈ ∅ )
7	6	con3i	⊢ ( ¬ 𝑥 ∈ ∅ → ¬ 𝑥 ∈ ( ∅ ∩ ( 0 [,) +∞ ) ) )
8	5 7	ax-mp	⊢ ¬ 𝑥 ∈ ( ∅ ∩ ( 0 [,) +∞ ) )
9		pm2.21	⊢ ( ¬ 𝑥 ∈ ( ∅ ∩ ( 0 [,) +∞ ) ) → ( 𝑥 ∈ ( ∅ ∩ ( 0 [,) +∞ ) ) → ( ∅ ‘ 𝑥 ) ∈ ℝ* ) )
10	8 9	ax-mp	⊢ ( 𝑥 ∈ ( ∅ ∩ ( 0 [,) +∞ ) ) → ( ∅ ‘ 𝑥 ) ∈ ℝ* )
11	10	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( ∅ ∩ ( 0 [,) +∞ ) ) ) → ( ∅ ‘ 𝑥 ) ∈ ℝ* )
12	1 3 4 11	liminfval3	⊢ ( ⊤ → ( lim inf ‘ ( 𝑥 ∈ ∅ ↦ ( ∅ ‘ 𝑥 ) ) ) = -𝑒 ( lim sup ‘ ( 𝑥 ∈ ∅ ↦ -𝑒 ( ∅ ‘ 𝑥 ) ) ) )
13	12	mptru	⊢ ( lim inf ‘ ( 𝑥 ∈ ∅ ↦ ( ∅ ‘ 𝑥 ) ) ) = -𝑒 ( lim sup ‘ ( 𝑥 ∈ ∅ ↦ -𝑒 ( ∅ ‘ 𝑥 ) ) )
14		mpt0	⊢ ( 𝑥 ∈ ∅ ↦ ( ∅ ‘ 𝑥 ) ) = ∅
15	14	fveq2i	⊢ ( lim inf ‘ ( 𝑥 ∈ ∅ ↦ ( ∅ ‘ 𝑥 ) ) ) = ( lim inf ‘ ∅ )
16		mpt0	⊢ ( 𝑥 ∈ ∅ ↦ -𝑒 ( ∅ ‘ 𝑥 ) ) = ∅
17	16	fveq2i	⊢ ( lim sup ‘ ( 𝑥 ∈ ∅ ↦ -𝑒 ( ∅ ‘ 𝑥 ) ) ) = ( lim sup ‘ ∅ )
18		limsup0	⊢ ( lim sup ‘ ∅ ) = -∞
19	17 18	eqtri	⊢ ( lim sup ‘ ( 𝑥 ∈ ∅ ↦ -𝑒 ( ∅ ‘ 𝑥 ) ) ) = -∞
20	19	xnegeqi	⊢ -𝑒 ( lim sup ‘ ( 𝑥 ∈ ∅ ↦ -𝑒 ( ∅ ‘ 𝑥 ) ) ) = -𝑒 -∞
21		xnegmnf	⊢ -𝑒 -∞ = +∞
22	20 21	eqtri	⊢ -𝑒 ( lim sup ‘ ( 𝑥 ∈ ∅ ↦ -𝑒 ( ∅ ‘ 𝑥 ) ) ) = +∞
23	13 15 22	3eqtr3i	⊢ ( lim inf ‘ ∅ ) = +∞