# Metamath Proof Explorer

## Theorem liminflelimsup

Description: The superior limit is greater than or equal to the inferior limit. The second hypothesis is needed (see liminflelimsupcex for a counterexample). The inequality can be strict, see liminfltlimsupex . (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses liminflelimsup.1 $⊢ φ → F ∈ V$
liminflelimsup.2 $⊢ φ → ∀ k ∈ ℝ ∃ j ∈ k +∞ F j +∞ ∩ ℝ * ≠ ∅$
Assertion liminflelimsup $⊢ φ → lim inf ⁡ F ≤ lim sup ⁡ F$

### Proof

Step Hyp Ref Expression
1 liminflelimsup.1 $⊢ φ → F ∈ V$
2 liminflelimsup.2 $⊢ φ → ∀ k ∈ ℝ ∃ j ∈ k +∞ F j +∞ ∩ ℝ * ≠ ∅$
3 oveq1 $⊢ k = i → k +∞ = i +∞$
4 3 rexeqdv $⊢ k = i → ∃ j ∈ k +∞ F j +∞ ∩ ℝ * ≠ ∅ ↔ ∃ j ∈ i +∞ F j +∞ ∩ ℝ * ≠ ∅$
5 oveq1 $⊢ j = l → j +∞ = l +∞$
6 5 imaeq2d $⊢ j = l → F j +∞ = F l +∞$
7 6 ineq1d $⊢ j = l → F j +∞ ∩ ℝ * = F l +∞ ∩ ℝ *$
8 7 neeq1d $⊢ j = l → F j +∞ ∩ ℝ * ≠ ∅ ↔ F l +∞ ∩ ℝ * ≠ ∅$
9 8 cbvrexvw $⊢ ∃ j ∈ i +∞ F j +∞ ∩ ℝ * ≠ ∅ ↔ ∃ l ∈ i +∞ F l +∞ ∩ ℝ * ≠ ∅$
10 9 a1i $⊢ k = i → ∃ j ∈ i +∞ F j +∞ ∩ ℝ * ≠ ∅ ↔ ∃ l ∈ i +∞ F l +∞ ∩ ℝ * ≠ ∅$
11 4 10 bitrd $⊢ k = i → ∃ j ∈ k +∞ F j +∞ ∩ ℝ * ≠ ∅ ↔ ∃ l ∈ i +∞ F l +∞ ∩ ℝ * ≠ ∅$
12 11 cbvralvw $⊢ ∀ k ∈ ℝ ∃ j ∈ k +∞ F j +∞ ∩ ℝ * ≠ ∅ ↔ ∀ i ∈ ℝ ∃ l ∈ i +∞ F l +∞ ∩ ℝ * ≠ ∅$
13 2 12 sylib $⊢ φ → ∀ i ∈ ℝ ∃ l ∈ i +∞ F l +∞ ∩ ℝ * ≠ ∅$
14 1 13 liminflelimsuplem $⊢ φ → lim inf ⁡ F ≤ lim sup ⁡ F$