Metamath Proof Explorer

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 ⊢ Ⅎ x ⊤
2 0ex ⊢ ∅ ∈ V
3 2 a1i ⊢ ⊤ → ∅ ∈ V
4 0red ⊢ ⊤ → 0 ∈ ℝ
5 noel ⊢ ¬ x ∈ ∅
6 elinel1 ⊢ x ∈ ∅ ∩ 0 +∞ → x ∈ ∅
7 6 con3i ⊢ ¬ x ∈ ∅ → ¬ x ∈ ∅ ∩ 0 +∞
8 5 7 ax-mp ⊢ ¬ x ∈ ∅ ∩ 0 +∞
9 pm2.21 ⊢ ¬ x ∈ ∅ ∩ 0 +∞ → x ∈ ∅ ∩ 0 +∞ → ∅ ⁡ x ∈ ℝ *
10 8 9 ax-mp ⊢ x ∈ ∅ ∩ 0 +∞ → ∅ ⁡ x ∈ ℝ *
11 10 adantl ⊢ ⊤ ∧ x ∈ ∅ ∩ 0 +∞ → ∅ ⁡ x ∈ ℝ *
12 1 3 4 11 liminfval3 ⊢ ⊤ → lim inf ⁡ x ∈ ∅ ⟼ ∅ ⁡ x = − lim sup ⁡ x ∈ ∅ ⟼ − ∅ ⁡ x
13 12 mptru ⊢ lim inf ⁡ x ∈ ∅ ⟼ ∅ ⁡ x = − lim sup ⁡ x ∈ ∅ ⟼ − ∅ ⁡ x
14 mpt0 ⊢ x ∈ ∅ ⟼ ∅ ⁡ x = ∅
15 14 fveq2i ⊢ lim inf ⁡ x ∈ ∅ ⟼ ∅ ⁡ x = lim inf ⁡ ∅
16 mpt0 ⊢ x ∈ ∅ ⟼ − ∅ ⁡ x = ∅
17 16 fveq2i ⊢ lim sup ⁡ x ∈ ∅ ⟼ − ∅ ⁡ x = lim sup ⁡ ∅
18 limsup0 ⊢ lim sup ⁡ ∅ = −∞
19 17 18 eqtri ⊢ lim sup ⁡ x ∈ ∅ ⟼ − ∅ ⁡ x = −∞
20 19 xnegeqi ⊢ − lim sup ⁡ x ∈ ∅ ⟼ − ∅ ⁡ x = − −∞
21 xnegmnf ⊢ − −∞ = +∞
22 20 21 eqtri ⊢ − lim sup ⁡ x ∈ ∅ ⟼ − ∅ ⁡ x = +∞
23 13 15 22 3eqtr3i ⊢ lim inf ⁡ ∅ = +∞