This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem liminfvald

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

Ref Expression
Hypotheses liminfvald.1 ⊢ φ → F ∈ V
liminfvald.2 ⊢ G = k ∈ ℝ ⟼ inf F k +∞ ∩ ℝ * ℝ * <
Assertion liminfvald ⊢ φ → lim inf ⁡ F = sup ran ⁡ G ℝ * <

Proof

Step Hyp Ref Expression
1 liminfvald.1 ⊢ φ → F ∈ V
2 liminfvald.2 ⊢ G = k ∈ ℝ ⟼ inf F k +∞ ∩ ℝ * ℝ * <
3 2 liminfval ⊢ F ∈ V → lim inf ⁡ F = sup ran ⁡ G ℝ * <
4 1 3 syl ⊢ φ → lim inf ⁡ F = sup ran ⁡ G ℝ * <